Symptom

You know reductions (T017): to prove your problem hard, reduce a known-hard problem to it. Fine. But that begs the obvious question, and it is the question a sharp colleague asks the first time you use the technique.

Where does the first hard problem come from?

Every hardness proof in the literature is a chain of reductions, and chains need a first link. If every NP-hardness result is “reduce from something already known NP-hard,” the entire edifice is circular unless somebody, once, proved a problem NP-hard from the definition. Somebody did, twice independently — Cook in Toronto in 1971 and Levin in Moscow, working in isolation behind the Iron Curtain — and the argument is the technical heart of the field.

The practical version of the symptom is quieter: you are wondering why SAT solvers are the universal tool. Why does everyone encode scheduling, verification, planning, and dependency resolution into Boolean satisfiability rather than building a specialized search? The answer is this theorem. SAT is not one hard problem among many. It is the problem that is computation, written down.

Statement

SAT is NP-complete. That is, SAT is in NP, and every language in NP reduces to SAT in polynomial time.

3-SAT is NP-complete too, where every clause has exactly three literals, which is the version everyone actually reduces from.

Unpacking “every language in NP reduces to SAT”: for any problem with efficiently checkable certificates — any problem at all, including ones nobody has thought of — there is a polynomial-time procedure converting its instances into Boolean formulas that are satisfiable exactly when the original instance is a yes. Boolean logic is expressive enough to encode arbitrary bounded computation, and that is the real content.

The consequence for practice: a polynomial SAT algorithm gives a polynomial algorithm for everything in NP. This is why SAT is the reduction target of choice in both directions — to prove hardness you reduce from it, and to solve your problem you reduce to it and call a solver.

Argument

SAT is in NP. The certificate is the satisfying assignment; checking it is one pass over the formula. Trivial, and worth stating only because completeness requires both halves.

Every NP problem reduces to SAT: the tableau construction. Let $L \in$ NP, decided by a nondeterministic machine $M$ in time $n^k$. Given input $w$, we build a formula satisfiable exactly when $M$ has an accepting computation.

Picture the computation as a table — Cook’s tableau — with $n^k$ rows (one per time step) and $n^k$ columns (one per tape cell, since in $n^k$ steps the head cannot move further). Each cell holds a tape symbol, or a state marker if the head is there. An accepting computation is precisely a correctly filled table.

Introduce a Boolean variable $x_{i,j,s}$ meaning “cell $(i,j)$ contains symbol $s$.” There are polynomially many. Now write four groups of clauses:

  • Well-formed. Each cell holds exactly one symbol: at least one ($\bigvee_s x_{i,j,s}$) and at most one ($\neg x_{i,j,s} \vee \neg x_{i,j,t}$ for $s \ne t$).
  • Start. Row 1 encodes the initial configuration: start state, input $w$, blanks after.
  • Accept. Some cell somewhere contains the accepting state.
  • Move. This is the only interesting one. Every consecutive pair of rows must be related by a legal transition of $M$.

The local-window trick, which is the whole idea. Checking that row $i+1$ legally follows row $i$ sounds global, but it is not: a Turing machine changes only the cell under the head and its immediate neighbourhood. So it suffices to check every $2 \times 3$ window — two rows, three adjacent columns — independently. A window is legal if its contents are consistent with some transition of $M$, and legality is a finite condition over a finite alphabet, so it is a constant-size Boolean formula. If every window is legal, the whole transition is legal; if any is not, it is not.

That local check is the reason the reduction is polynomial. Computation is a local process — each step touches a bounded neighbourhood — and locality is exactly what a conjunction of small clauses expresses. The formula has $O(n^{2k})$ variables and clauses, and is constructible in polynomial time by a straightforward program that never runs $M$ at all.

Satisfying assignments correspond exactly to accepting computations. So $w \in L \iff \phi_w \in \text{SAT}$.

From SAT to 3-SAT. Convert each clause to CNF, then split long clauses using fresh variables: $(a \vee b \vee c \vee d)$ becomes $(a \vee b \vee z) \wedge (\neg z \vee c \vee d)$, which is satisfiable exactly when the original is. Repeat. Linear blowup, and now every clause has three literals. The Tseytin transformation does the same job for arbitrary circuits in linear size, and it is what every real encoder uses.

Levin’s version. Levin proved essentially the same result independently and published a short abstract in 1973, framing it in terms of search problems rather than decision problems — closer to what people actually want. The Soviet and Western literatures met later, and the joint name is the field’s acknowledgement of a genuinely independent discovery.

Why this made the catalogue possible. With one NP-complete problem in hand, transitivity does the rest. Karp’s 1972 paper (T028) reduced SAT to 21 problems in one stroke, and the count is now in the thousands. Everything downstream is this theorem plus composition.

Forbids

A polynomial SAT algorithm that does not collapse NP into P. SAT’s completeness means solving it solves everything in NP. Any claimed polynomial-time SAT algorithm is a claim of P = NP.

Proving your problem is not NP-hard by showing it is unlike SAT. Superficial dissimilarity is not evidence; the tableau construction shows that utterly unrelated-looking problems encode the same thing.

Efficiently deciding satisfiability of general circuits, unless P = NP. Circuit-SAT is NP-complete, which is why symbolic execution and equivalence checking have exponential worst cases, and why your verification tool sometimes hangs.

A general polynomial procedure for finding proofs of bounded length. Cook’s original motivation: proof search for bounded-length proofs is NP-complete, so automated theorem proving is hard in the worst case by this theorem specifically.

Does not forbid

It does not make SAT hard in practice, and the gap is enormous. MiniSat, Kissat, and CaDiCaL routinely solve industrial instances with millions of variables. CDCL — conflict-driven clause learning, with unit propagation, VSIDS activity heuristics, watched literals, and restarts — exploits structure that worst-case theory cannot see. SAT is the backbone of hardware equivalence checking at Intel, of apt and Dart’s pub dependency resolution, and of symbolic execution engines. The theorem tells you SAT is universal, and universality is precisely why investing in one solver pays off across every domain.

It does not mean all SAT instances are equally hard. Random 3-SAT has a sharp phase transition at a clause-to-variable ratio around 4.27: below it instances are almost all satisfiable and easy, above it almost all unsatisfiable and easy to refute, and only near the threshold are they hard. Industrial instances are almost never near it, which is a large part of why solvers work.

It does not make every restricted SAT hard. 2-SAT is in P via implication graphs and strongly connected components (linear time), Horn-SAT is in P by unit propagation and is the basis of Datalog and Prolog inference, and XOR-SAT is Gaussian elimination. Schaefer’s dichotomy theorem is the sharp statement: every Boolean constraint satisfaction problem is either in P or NP-complete, with exactly six tractable cases and nothing in between. That is an unusually complete answer to “which restrictions help.”

It does not mean encoding to SAT is always the right move. SMT solvers keep theories — arithmetic, arrays, bit-vectors, uninterpreted functions — at the native level instead of bit-blasting, and Z3 usually beats a hand-rolled SAT encoding badly on such problems. Integer programming solvers beat SAT on optimization. The reduction proves possibility; the engineering question of which encoding to use is separate and often goes the other way.

It does not say anything about approximation or counting. Cook–Levin is about decision. Counting satisfying assignments (#SAT) is #P-complete and strictly harder than deciding, which is Toda’s theorem territory, and it matters because probabilistic inference is a counting problem rather than a decision one.

Boundary

  • What made SAT the right universal problem. The tableau is a table of local constraints, and CNF is the natural language of local constraints. Any formalism expressive enough to state “these adjacent cells are consistent” would work, which is why tiling problems and circuit value problems are also complete.
  • The Tseytin transformation is the practical version. Naive CNF conversion is exponential; Tseytin introduces a variable per gate and produces linear-size equisatisfiable CNF. Everyone who encodes to SAT uses it, and knowing it exists is what makes reduction-to-SAT a practical technique rather than a theoretical one.
  • The Karp–Levin distinction. Cook used Turing reductions, Karp used many-one, and the modern definition follows Karp because many-one reductions give a finer theory. The naming convention “Karp reduction” comes from here.
  • Where the tableau reappears. The same construction proves the time-hierarchy-flavoured completeness results for other classes: bounded-space computation gives PSPACE-completeness of QBF, and alternating quantifiers give the polynomial hierarchy. The technique generalizes cleanly, which is another sign SAT was not an arbitrary choice.
  • The barriers apply here too (T030). The tableau argument is a simulation, so it relativizes. That is fine for proving completeness and useless for separating classes, which is exactly the dividing line the barrier results draw.