TAOCP Vol 4B: Combinatorial Algorithms, Part 2 · Week 123
TAOCP 7.2.2.2 Satisfiability (part 2): reading guide
Part 2 covers the basic solving algorithms: backtracking, unit propagation, watched literals for fast propagation, and lookahead solvers.
Time About 9 hours this week
Why it matters
Watched literals are one of the key engineering ideas that made SAT solvers fast. Implementing them teaches serious data structure design.
Before you start
- 7.2.2.2 part 1
How to approach it
Write a DPLL solver with unit propagation in C. Then add watched literals and measure the speedup on random 3-SAT instances near the hard ratio of about 4.26 clauses per variable.
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
- Bugs in watched-literal updates when a clause becomes unit or conflicting.