Week 125 of 125
TAOCP 7.2.2.2 and Vol
Sign up or sign in to tick these off and give this week a due date.
-
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.
-
Knuth Knuth Vol 4B review
The final review week: Volume 4B and the whole path.
Time About 5 hours this week
Why it matters
You made it. This is the week to look back at 125 weeks of work and decide what to go deeper on.
Before you start
- Everything
How to approach it
Write a short retrospective: what stuck, what did not, and which volume you would reread. Check Knuth's TAOCP page for the newest pre-fascicles of Vol 4C if you want more.
Exercises
Pick any exercise from any volume that you gave up on and finish it. Then celebrate.