Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs
summary
Finds that many DRAT proofs rely on spurious unit deletions: CDCL solvers (e.g. MiniSat-style solver-remove-satisfied) emit deletions that keep propagated literals alive, so operational checkers ignore them while the formal DRAT specification does not. Empirically about 60% (rising to 77% incorrect) of competition proofs are correct for the operational checkers but invalid per the spec. Fixes: avoid those deletions in solvers, implement a specified DRAT checker with trail pre‑processing and core‑first propagation to match performance, and produce three-valued semantics witness certificates to certify incorrect inferences.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 0:30General Pipeline
- 2:28Unit Classes
- 4:56Practical Issues
- 7:45Sat Solvers
- 11:15Red checkers
- 13:26DRAT certificates
- 15:43Conclusion
- 16:58Questions
related talks
01h 05mThe Power of Extended Resolution: A Practitioner's Perspective
15mTowards Proof Stability in SMT-based Program Verification
16mTesting Differential Privacy with Dual Interpreters
41mTotal Functions for Automated Reasoning:Building Terminating Theorem Provers
19mAutomated Verification of Fundamental Algebraic Laws
20mMRPHS: Enabling Transaction-level Deductive Formal Verification Through PDVL
19mDestructive E-Graph Rewrites
01h 34mFormal Logic Undressed