Skip to content

SAT Solvers

Abstract

Boolean satisfiability was the first problem ever proven NP-complete, the textbook emblem of computational intractability: in the worst case, deciding whether a logical formula can be made true takes time that explodes exponentially with its size. That is the theory. In practice, programs called SAT solvers now settle formulas with millions of variables in seconds, every day, inside the tools that verify microprocessors and find software bugs. The gap between “provably hard” and “routinely solved” is the whole story here, and closing it took forty years of engineering that theory did not predict.

The Problem That Defined Hardness

A Boolean formula is a tangle of variables joined by AND, OR, and NOT. Satisfiability (SAT) asks the plainest possible question: is there any assignment of true and false to the variables that makes the whole formula true? In 1971 Stephen Cook proved SAT NP-complete, the hardest problem in its class, the one every other NP problem reduces to. The naive method is to try all assignments, and with n variables there are 2ⁿ of them: fifty variables already exceed a quadrillion combinations. For decades SAT was cited in textbooks precisely as the thing you cannot do efficiently, the canonical intractable problem.

From Davis-Putnam to Backtracking

Work on actually solving it predates the hardness proof. In 1960 Martin Davis and Hilary Putnam published a procedure for testing satisfiability. Two years later Davis, with George Logemann and Donald Loveland, refined it into what is now called DPLL, the algorithm at the base of essentially every modern solver. DPLL is a smart backtracking search: guess a value for a variable, propagate the forced consequences (a clause with one unassigned literal forces that literal), and when the guesses lead to a contradiction, back up and try the other branch. Unit propagation and pure-literal elimination prune huge swaths of the search tree. DPLL is complete, meaning it always terminates with a correct yes or no, and for thirty years it was the state of the art, capable of formulas with hundreds of variables. Real engineering problems had millions.

The Trick That Changed Everything

The leap came in the 1990s with conflict-driven clause learning (CDCL). The insight: when the search hits a dead end, do not just backtrack, but analyze why it failed, distill the reason into a new clause, and add that clause to the formula so the solver never makes the same mistake again in any other part of the search. The solver learns from its own failures. GRASP, from João Marques-Silva and Karem Sakallah in 1996, introduced clause learning; then in 2001 a solver from Princeton called Chaff, built by a group including Sharad Malik, added a data structure (“two watched literals”) that made unit propagation staggeringly fast, plus a heuristic that focused the search on recently useful variables. Chaff was one to two orders of magnitude faster than anything before it, and it broke the problem open. MiniSat, released in 2003, distilled the whole approach into about 600 lines of readable C++ and became the template everyone learned from. Formulas with millions of variables became routine.

Why CDCL beats the exponential worst case on real inputs is still not fully understood theoretically. The instances that arise from actual engineering are not adversarial; they have structure, symmetry, and locality that clause learning exploits and that random worst-case instances lack. SAT solving is the clearest case in computing of a problem that is genuinely hard in the worst case and genuinely easy in practice, and the reconciliation is empirical: the hard instances exist, they just are not the ones anyone needs to solve.

What Runs on It

The payoff is industrial. Electronic design automation was the first big customer: when a chip has billions of transistors, you verify that the logic is correct by encoding “does this circuit ever produce a wrong output” as a giant SAT formula and asking a solver to find a counterexample or prove none exists. Every major processor is now checked this way, a direct response to the 1994 Pentium division bug that cost Intel around half a billion dollars. Bounded model checking, introduced by Armin Biere and colleagues in 1999, unrolls a hardware or software system for k steps and hands the result to a SAT solver to hunt for bugs. The approach generalized into SMT (satisfiability modulo theories) solvers like Microsoft Research’s Z3, which handle not just true/false variables but arithmetic and data structures, and which now sit inside program verifiers, symbolic execution engines, and the type checkers of some programming languages.

An annual SAT Competition, running since 2002, drove the improvement by pitting solvers against a common benchmark set, and year over year the solvable problem sizes climbed. The field is the standing counterexample to a naive reading of NP-completeness. “NP-complete” means no algorithm is fast on every input; it never meant no algorithm is fast on the inputs you actually have. A generation of engineers took the most notorious intractable problem in computer science and turned it into a utility you call from a library.

📚 Sources