TAOCP Vol 4B: Combinatorial Algorithms, Part 2 · Week 124
TAOCP 7.2.2.2 Satisfiability (part 3): reading guide
Part 3 covers conflict-driven clause learning (CDCL), the method behind modern solvers: learning new clauses from conflicts, non-chronological backjumping, restarts and clause database management.
Time About 10 hours this week
Why it matters
CDCL is why SAT went from theory to industrial tool. It is a beautiful example of an algorithm learning from its own failures.
Before you start
- 7.2.2.2 part 2
How to approach it
Read slowly and trace a conflict analysis by hand on a small formula. Extend your DPLL solver with clause learning if you have the energy; otherwise study a small open-source CDCL solver.
Exercises
Work every exercise rated 10 to 20; most are about tracing the algorithm by hand or tweaking one step, which is exactly the skill you want. Pick one or two rated 20 to 25 that involve modifying the algorithm and implement your modification in a real language with tests. Skip HM exercises unless you enjoy calculus, and treat anything rated 40+ as a research problem, not homework.
Traps
- Getting the implication graph wrong when analyzing conflicts.