发表机构
University of Toronto; Georgia Institute of Technology（多伦多大学; 佐治亚理工学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对ZkUnsat零知识UNSAT验证扩展性受限问题，提出归一化链接预处理技术，固定归结链长度消除泄露并降低内存，在SAT 2002基准上认证实例数提升62%，内存降至25%以下。
AI 中文摘要
UNSAT证明是形式化验证和软件保证中的标准原语。在许多现实场景中，证明本身编码了专有或安全敏感信息，使得公开披露不可取。UNSAT的零知识认证解决了这一矛盾：它使证明者能够说服验证者不存在满足赋值，而不泄露除有效性之外的任何底层证明信息。Luo等人最近引入了ZkUnsat，该协议通过在零知识中证明弱化归结证明的有效性来实现这一目标。ZkUnsat展示了零知识认证的可行性；然而，其扩展到更大、更现实的实例的能力受到大量证明者内存开销的限制，从而限制了其实际应用性。受LRAT等UNSAT证明格式（这些格式支持高效的明文验证）进展的启发，我们提出了一种预处理技术，在不引入额外泄露的情况下提高ZkUnsat的效率。我们的方法对证明进行归一化，使得每个推导出的子句都由固定公共长度k的归结链来证明。这消除了链长度泄露并减少了证明者的内存使用。当k=16时，我们的方法在SAT 2002竞赛基准上比基线ZkUnsat多认证约62%的实例。此外，对于相同数量的已认证实例，内存占用降至基线所需内存的25%以下。
英文摘要
Proofs of UNSAT are a standard primitive in formal verification and software assurance. In many real-world settings, the proof itself encodes proprietary or security-sensitive information, making public disclosure undesirable. Zero-knowledge certification of UNSAT addresses this tension: it enables a prover to convince a verifier that no satisfying assignment exists, without revealing anything about the underlying proof beyond its validity. Luo et al. recently introduced ZkUnsat, a protocol that achieves this goal by proving the validity of a weakened resolution proof in zero knowledge. ZkUnsat demonstrates the feasibility of zero-knowledge certification; however, its scalability to larger, real-world instances is constrained by substantial prover memory overhead, limiting its real-world applicability. Motivated by advances in UNSAT proof formats such as LRAT, which enable efficient plain-text verification, we present a preprocessing technique that improves the efficiency of ZkUnsat without introducing additional leakage. Our approach normalizes the proof so that each derived clause is justified by a resolution chain of fixed public length k. This eliminates chain-length leakage and reduces prover memory usage. With k = 16, our method certifies roughly 62% more instances than baseline ZkUnsat on the SAT 2002 competition benchmarks. Furthermore, for an equivalent number of certified instances, the memory footprint drops to under 25% of that required by the baseline.
