Proving UNSAT in Zero Knowledge

on YouTube ↗48m

" summary

A practical zero‑knowledge protocol proves propositional UNSAT by encoding clauses as polynomials and checking resolution steps as algebraic relations over a finite field; the implementation uses polynomial encoding of clauses plus authenticated evaluations at random points to verify resolvents without revealing formula or proof and demonstrates real driver‑verification instances in about 300 seconds. The prototype handles proofs up to about width 1,000 and length 600K before running out of memory; read‑only array checks and MPC variants are used for other components.

AI-written summary · about

" chapters (10)

1. 0:00Motivation and context
2. 2:56Defining the problem
3. 5:42Resolution proof basics
4. 10:25Zero knowledge foundations
5. 18:59Privacy-preserving protocol
6. 22:35Polynomial encoding approach
7. 28:39Fetching clauses in ZK
8. 29:50Performance and benchmarking
9. 35:01Future directions
10. 40:18Q&A and conclusion

" related talks

• 33mAn Introduction to Zero Knowledge ProofsShubham Patil, Keertana Ganesh · DevOpsDays Geneva 2023
• 01h 13mA Zero-Knowledge PCP TheoremNicholas Spooner · Proofs (Simons Institute)
• 01h 09mProofs - Practice 1Justin Thaler · Cryptography 10 Years Later: Obfuscation, Proof Systems, and Secure Computation Boot Camp 2025
• 49mLattice-Based Zero Knowledge and ApplicationsDaniele Micciancio · ZK Day 2019: Blockchains, Micropayments and Zero Knowledge
• 23mZKBoo: Faster Zero-Knowledge for Boolean CircuitsIrene Giacomelli, Jesper Madsen, Claudio Orlandi · USENIX Security '16
• 01h 06mLattice-based Zero-knowledge ProofsVadim Lyubashevsky · Quantum and Lattices Joint Reunion Workshop
• 38mNew Techniques for Zero-Knowledge: Leveraging Inefficient Provers to Reduce Assumptions, ...Dana Dachman-Soled · Minimal Complexity Assumptions for Cryptography 2023
• 28mZero Knowledge Proofs and Their Future ApplicationsElad Verbin · Web3 Summit 2018