A Peek Inside SAT Solvers
summary
Explains how real SAT solvers turn CNF encodings into fast answers by combining conflict driven clause learning with clever propagation like two-watched literals, heuristics (VSIDS), phase saving and periodic restarts; typical benchmarks are ~3,000 variables and 10,000 clauses and many get solved in minutes while one solver emitted a 2 terabyte unsat proof; shows practical encodings (one hot for Sudoku), points to Zchaff/Z3 and Super (super optimizing LLVM) and reports that these techniques make formerly intractable instances solvable.
AI-written summary · about
chapters (12)
- 0:00Intro
- 1:50Outline
- 5:11Other Applications
- 7:01Encoding
- 9:30DepthFirst Search
- 12:39D PLL
- 15:01Unit Propagation
- 17:31Conflict Driven Learning
- 25:34Legally Binding
- 27:41Current Research
- 31:04SuperOptimizing LLVM
- 34:04Sage Wisdom
related talks
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
21mMassive proofs for the masses
15mSatune: Synthesizing Efficient SAT Encoders
22mSatisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
35mThe Mastermind behind Refinement Types
15mInter-theory Dependency Analysis for SMT String Solvers
30mAnalyzing Programs with SMT Solvers
54mUse a Rust SAT Solver to play better pickleball!