A Roadmap for the Next Phase of SAT Research
summary
Argues CDCL’s power comes from combining conflict-driven learning with conflict-driven branching, conjectures that many human-created CNF encodings have surprisingly short resolution refutations, and shows a working prototype TabularaSAT prototype plus a timestamped database that ran 11 families (mostly from SAT competitions) with 11 families × 10 instances, some formulas having up to millions of variables. Calls for a community-curated, persistent benchmark corpus and controlled experiments (change one option at a time: core/minisat/parfait/semifreddo/stracciatella) to correlate solver features with formula structure.
AI-written summary · about
chapters (17)
- 0:00SAT research roadmap intro
- 2:12Theory vs practice in SAT
- 3:36CDCL history and performance
- 8:16GRASP solver origin
- 9:00Phase transition in SAT
- 12:17Conflict-driven satisfiability
- 15:27Why CDCL solvers excel
- 17:12Structural metrics in SAT instances
- 20:28Critique of SAT competition
- 27:14Scientific approach to SAT
- 32:29Structured SAT research proposal
- 41:55Introducing tabularasat
- 45:49Analyzing tabularasat results
- 47:16Family-specific SAT performance
- 50:57Theorists vs practitioners
- 55:35Science vs entertainment in SAT
- 1:01:13Q&A
related talks
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
34mAbstract Interpretation, Software Model Checking, and Beyond - A Celebration of the(…)
31mGenerating Constraint Programs for Variability Model Reasoning: A DSL and Solver-...
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...
40mUtilizing Structure in Combinatorial Solving and Reasoning
16mSoftware Model Checking via Summary-Guided Search
36mSpecification-Guided Component-Based Synthesis from Effectful Libraries
28mBounded Model Checking of PLC ST Programs using Rewriting Modulo SMT