Scaling zero knowledge UNSAT verification reduces memory use and boosts certification
Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
Cryptography and SecurityLogic in Computer Science
Summary
Checking that certain logic puzzles have no solutions is important for software safety, but sharing how you proved this can reveal secrets. The paper improves a method that lets one prove no solution exists without revealing any details, but previous ways used too much memory making them hard to use. The authors propose a way to standardize part of the proof, cutting memory needs and allowing more puzzles to be checked efficiently. This means privacy-preserving proof methods can work better on bigger, real problems.
What this means in practice
- •For software verification teams: Verify software correctness proofs without exposing proprietary implementation details using reduced-memory zero knowledge proofs.
- •For security auditing teams: Certify absence of security vulnerabilities in code via private proofs that use less memory and verify faster.
Authors
Ashwin Karthikeyan, Ethan Kharitonov, Kuldeep S. Meel, Anwar Hithnawi
Abstract
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.