3-SAT phase transition (Kirkpatrick & Selman 1994): for random 3-SAT formulas with n variables and m=αn clauses, the probability of satisfiability transitions sharply from ≈1 to ≈0 near α_c ≈ 4.267.
Hardest instances cluster at the threshold — exponential time for DPLL. Below: easy-SAT (large satisfying fraction). Above: easy-UNSAT (constraint propagation proves it quickly). DPLL algorithm: unit propagation → pure literal → branch. Backtrack search, complete but exponential worst-case.