Progress in Symbolic Satisfiability Solving
Talkat 50 Years of Satisfiability: The Centrality of SAT in the Theory of Computing · 2021-02-11..05-13
summary
Field-wide claim: CDCL remains the single algorithmic backbone, tied to resolution (the weakest proof system) despite scaling SAT to industrial instances with over a million variables. A different route builds symbolic decision diagrams and implements BDDSAT (early results: worse than ZCHAFF on many benchmarks but strong on structured cases like the mutilated checkerboard), then weighted versions as ADDMC (adds ~150 solved instances to the virtual-best solver, ~10% gain), and tree-decomposition dynamic programming as DPMC (ties first in the weighted model-counting track; works well when treewidth ≲50). The core technique is aggressive variable elimination: join lazily, project eagerly.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:52The SAT Revolution
- 2:36Raining on The Party
- 3:56Complexity Theory and Proofs
- 6:42Proof Complexity and Satisfiability Solving
- 10:45CSP Proofs
- 18:05Boolean Constraint Representation
- 21:08BDDs vs. Resolution
- 24:00BDD Proofs for SAT Solving
- 26:15Clause Reordering
- 28:43Symbolic Approach vs. Search
- 30:37Reduced Ordered Algebraic Decision Diagrams
- 33:57Back to Tree Decompositions
- 37:46Discussion