Week 122 of 125
TAOCP 7.2.2.2 Satisfiability (part 1)
Sign up or sign in to tick these off and give this week a due date.
-
Part 1 covers the opening of the giant SAT section: what SAT is, and a long tour of example problems encoded as SAT (coloring, scheduling, puzzles, circuits, and more), showing how to translate problems into clauses.
Time About 9 hours this week
Why it matters
Modern SAT solvers are astonishingly good, and knowing how to encode a problem as SAT lets you solve things that look impossible: package dependency resolution, hardware verification, scheduling.
Before you start
- 7.1.1 Boolean Basics
- 7.2.2 Backtrack Programming
How to approach it
Install a real solver (MiniSat or CaDiCaL), write DIMACS files for a couple of the example problems, and solve them. Focus on encoding tricks.
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
- Naive encodings of "at most one" constraints blow up quadratically; read the encoding tricks.