SAT solving in a nutshell
The Boolean satisfiability (SAT) problem asks: given a formula, is there an assignment of 0/1 values to its variables that makes it true? It is the canonical NP-complete problem, yet modern solvers routinely handle formulas with millions of variables from real hardware. Almost every modern formal engine is built on top of a SAT solver.
Conjunctive normal form
Solvers take formulas in CNF: an AND of clauses, each clause an OR of literals. Any circuit can be
converted to CNF in linear size by giving each gate output a variable (the Tseitin encoding). For example, an AND gate
g = x · y becomes three clauses: (¬g ∨ x), (¬g ∨ y), (g ∨ ¬x ∨ ¬y).
A worked example
Is this formula satisfiable?
(p ∨ q) · (¬p ∨ r) · (¬q ∨ r) · (¬r ∨ s) · (¬s ∨ ¬p)
- Decide p = 1. Clause 2 becomes (r) — a unit clause — so r = 1 is forced.
- Propagate r = 1: clause 4 forces s = 1.
- Propagate s = 1: clause 5 becomes (¬p) but p = 1 — conflict.
- Learn from the conflict: p = 1 always leads to failure, so add the clause (¬p) and backtrack.
- Now p = 0: clause 1 forces q = 1; clause 3 forces r = 1; clause 4 forces s = 1; clause 5 is satisfied by ¬p.
Result: satisfiable with p=0, q=1, r=1, s=1. In formal terms, that satisfying assignment is a counterexample (or a cover trace) once the formula encodes "the property is violated".
From DPLL to CDCL
Steps 1–3 (decide, propagate, backtrack) are the classic DPLL procedure. Step 4 — analysing the conflict and adding a learned clause so the same mistake is never repeated — is the heart of conflict-driven clause learning (CDCL). Together with clever data structures (watched literals), restarts and decision heuristics, CDCL is why SAT went from toy problems to industrial workhorse in the late 1990s and early 2000s.