TAOCP Vol 4B: Combinatorial Algorithms, Part 2 · Week 125
TAOCP 7.2.2.2 Satisfiability (part 4): reading guide
Part 4 covers the rest: local search methods like WalkSAT, message passing, preprocessing and simplification, encoding choices, and the history and outlook of SAT solving.
Time About 8 hours this week
Why it matters
Local search solves huge satisfiable instances fast, and preprocessing is a big part of real-world solver performance.
Before you start
- 7.2.2.2 part 3
How to approach it
Implement WalkSAT and compare it with your DPLL solver on satisfiable and unsatisfiable random instances. Skim the more specialized subsections.
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
- Expecting local search to prove unsatisfiability. It cannot.