The Power of Extended Resolution: A Practitioner's Perspective
summary
Extended resolution is used to attach concise, checkable proofs to non‑CDCL reasoning: a BDD‑based proof generator emits DRAT/LRAT clauses so Gaussian elimination on parity constraints and pseudo‑Boolean steps integrate with CDCL checkers. A parity benchmark that stalls KISSAT at n≈42 runs to about 10,000 variables with the BDD approach. Knowledge‑compilation experiments use D4 on 180 instances (124 solved), the generator produces two‑sided proofs for 108, hits limits when defining clauses reach 2.7 billion clauses, overflowing 32‑bit IDs.
AI-written summary · about
chapters (7)
- 0:00The case for checkable proofs
- 3:02SAT solving and resolution
- 7:45Extended resolution power
- 15:28BDDs for proof generation
- 28:41Pseudo-Boolean formulas
- 39:25Knowledge compilation
- 56:22Questions and discussion
related talks
20mFrying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs
19mPanel: Compilation Frameworks
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
21mMassive proofs for the masses
35mA Peek Inside SAT Solvers
13mInteractive Bit Vector Reasoning using Verified Bitblasting
41mLiving inside a Theorem Proving Universe
29mA Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic