SATisfying answers to difficult questions!
summary
Overview of concrete methods and limits: explains how problems become CNF and shows a Sudoku encoding with nine Booleans per cell, implements DPLL with unit propagation and pure literal elimination and then upgrades to CDCL that learns clauses and backjumps non-chronologically, demonstrates a stochastic approach WalkSAT that is parallelizable on GPUs but cannot prove unsatisfiability, and contrasts pure SAT with SMT (mentions Z3 and CVC yees boctor Etc) for arithmetic-heavy puzzles like SEND+MORE=MONEY.
AI-written summary · about
chapters (7)
- 0:00SAT solvers and NP-complete
- 1:38Boolean satisfiability explained
- 3:02DPL and unit propagation
- 5:27Conflict-driven clause learning
- 7:17WalkSAT and stochastic search
- 8:20SMT theories in SAT solvers
- 9:45Summary and resources
related talks
44mAutomated Scientific Discovery Using Insights from Problem Structure
32mExplaining SAT Solving Using Causal Reasoning
34mSolving Problems Declaratively
20mFunction synthesis for maximizing model counting
29mLet our optima combine!
18mSAT Beyond Boolean Interpretations
17mSynthesizing MILP Constraints for Efficient and Robust Optimization
41mCounting Solutions to Random CNF Formulas