Proving UNSAT in Zero Knowledge

Channel:
United States Simons Institute for the Theory of Computing
Subscribers:
68,700
Published on ● Video Link: https://www.youtube.com/watch?v=p3oYJJjR7M0


Duration: 47:56
412 views
3

Ning Luo (Northwestern University)
https://simons.berkeley.edu/talks/ning-luo-northwestern-university-2023-04-21
Satisfiability: Theory, Practice, and Beyond

Zero-Knowledge (ZK) protocols have been extensively researched in recent years, with a focus on finding efficient protocols for problems in NP, such as proving the satisfiability of a Boolean formula. However, less attention has been given to proving the unsatisfiability of a given formula without revealing any related proofs or even the formula itself. In this talk, I will talk about our work on a highly efficient zero-knowledge protocol for proving the unsatisfiability of Boolean formulas in propositional logic. Our protocol is based on polynomial equivalence checking, which allows for the verification of a resolution proof of unsatisfiability in a zero-knowledge setting. We have implemented this protocol and have demonstrated its effectiveness by checking the unsatisfiability of real-world formulae used for verifying system drivers within just 300 seconds. This work was published in the CCS 2022 and was awarded a distinguished paper award.



Other Videos By Simons Institute for the Theory of Computing


2023-04-26Robust Multivalid Conformal Prediction
2023-04-25Calibration: Unbiased Answers to Arbitrary Questions
2023-04-25Validity of Decision Making Algorithms
2023-04-25Multi-Group Fairness and Loss Minimization
2023-04-25Multicalibration and Outcome Indistinguishability II
2023-04-24Multicalibration and Outcome Indistinguishability I
2023-04-22SAT Beyond Boolean Interpretations
2023-04-22Unification of SAT, Constraint Programming, and Pseudo-Boolean Solving: A Personal Story
2023-04-22Explaining SAT Solving Using Causal Reasoning
2023-04-22Knowledge Compilation for Quantification and Synthesis
2023-04-22Proving UNSAT in Zero Knowledge
2023-04-22Analysis of Core-Guided MaxSat Using Cores and Correction Sets
2023-04-21Homomorphism Counts: Expressive Power and Query Algorithms
2023-04-21Proof Logging for Constraint Programming
2023-04-21Proof Logging for MaxSAT – The Past, The Present and The Future
2023-04-21Certified Static and Dynamic Symmetry Breaking
2023-04-21Trustworthy Automated Reasoning
2023-04-21MCSat Approaches for Solving Non-linear Modular Arithmetic
2023-04-21Reactive Synthesis Empowered by Logical Reasoning
2023-04-20The Power of Extended Resolution: A Practitioner's Perspective
2023-04-20Exploiting Combinatorial Structure in Constraint Programming: ...


Tags:
Simons Institute
theoretical computer science
UC Berkeley
Computer Science
Theory of Computation
Theory of Computing
Satisfiability: Theory Practice and Beyond
Ning Luo