Short Proofs in Strong Proof Systems
Talkat 50 Years of Satisfiability: The Centrality of SAT in the Theory of Computing · 2021-02-11..05-13
summary
Claims that stronger, interference-based clausal proof systems let SAT solvers produce exponentially shorter certificates than resolution, using techniques like reverse unit propagation and the positive reduct to check redundancy and block assignments. Implementations add blocked clauses and SDCL-style clause learning to CDCL engines, and verified checkers exist in ACL2/Isabelle/Coq/CakeML. Results include linear-size proofs for pigeonhole problems (only unit and binary clauses) and practical speedups via block clause elimination; some structured cases like mutilated chessboards improve but remain heuristic-dependent.
AI-written summary · about
chapters (12)
- 0:00Intro
- 3:23Certifying Satisfiability and Unsatisfiability
- 6:22Resolution Proofs
- 8:19Clausal Proofs
- 10:39Reverse Unit Propagation
- 19:20Short Proofs of Pigeon Hole Formulas Cook 1967
- 23:26Blocked Clause Addition and Blocked Clause Elimination
- 24:55DRAT: An Interference-Based Proof System
- 27:30Proof Search in Strong Proof Systems
- 42:00Finding Conditional Autarkies
- 44:57Satisfaction-Driven Clause Learning Heule, Kiesl, Biere '17
- 50:32Practical Challenges