SAT Theory
3-SAT: Each clause has exactly 3 literals. First NP-complete problem (Cook-Levin 1971).
Phase transition: Random 3-SAT near ratio α = clauses/vars ≈ 4.267 is hardest. Below: almost always SAT. Above: almost always UNSAT.
DPLL algorithm (Davis-Putnam-Logemann-Loveland, 1962):
1. Unit propagation: if clause has 1 unassigned literal, force it
2. Pure literal: if a variable appears only positive or only negative, set it
3. Branch: pick unassigned variable, try T then F
4. Backtrack on conflict
Modern SAT solvers (MiniSAT, etc.) extend DPLL with CDCL (Conflict-Driven Clause Learning). Practical SAT solvers can handle millions of variables.
Phase Diagram