A 3-CNF formula is a conjunction of clauses, each a disjunction of three literals (a variable or its negation). It is satisfiable if some assignment of true/false to every variable makes every clause true.
phi = C1 AND C2 AND ... AND Cm, each Ci = (l1 OR l2 OR l3)
SAT <=> exists v: X -> {0,1} such that phi(v) = 1
DPLL(phi, assignment):
unit-propagate -> force literals from clauses with exactly 1 unassigned literal
if some clause is fully false -> CONFLICT, backtrack
if every clause has a true literal -> SAT, return assignment
else pick an unassigned x, branch:
DPLL(phi, assign x = false)
DPLL(phi, assign x = true)
3-SAT phase transition: hardest random instances cluster near m/n ~ 4.26
(clauses per variable) — below it almost everything is SAT, above it almost
everything is UNSAT, and the search tree explored here peaks right at 4.26.
- Variables — size of the formula; each level of the tree is one decision variable.
- Clause density — clauses-per-variable ratio; push it toward 4.26 to watch the tree explode with backtracking.
- Steps / second — how fast the solver's generator advances; pause any time to inspect the current branch.
- New formula — draws a fresh random 3-CNF instance and restarts the search from the root.
Real SAT/SMT solvers (MiniSat, Z3, CVC5) use exactly this DPLL skeleton, extended with clause learning (CDCL), watched literals and heuristics — the same backtracking-search shape scaled to millions of variables, underpinning hardware verification, scheduling and automated theorem proving.