Cook–Levin theorem
The cook–levin theorem establishes that the Boolean satisfiability problem is NP-complete. Equivalently, every decision problem whose affirmative instances admit certificates verifiable in polynomial time has a polynomial-time many-one reduction to Boolean satisfiability. The theorem therefore identifies satisfiability as a representative problem for the entire complexity class NP.
The result was proved by Stephen Cook in 1971 and independently formulated within a different computational framework by Leonid Levin in 1973. Its central construction encodes the bounded computation of a nondeterministic machine as a propositional formula. The formula is satisfiable exactly when the encoded machine has an accepting computation on the specified input.
Statement
Let (L) be a language in NP. There exists a polynomial-time computable function (f) such that, for every input string (x),
[ x\in L \quad\Longleftrightarrow\quad f(x)\in \mathrm{SAT}, ]
where (\mathrm{SAT}) denotes the set of satisfiable Boolean formulas. Thus,
[ L\leq_{\mathrm p}\mathrm{SAT}, ]
with (\leq_{\mathrm p}) denoting a polynomial-time many-one reduction.
The theorem has two components. Boolean satisfiability belongs to NP because a truth assignment constitutes a certificate whose validity can be checked in time polynomial in the formula length. Satisfiability is NP-hard because every polynomially bounded nondeterministic computation can be represented by a polynomial-size Boolean formula.
Several standard formulations replace general Boolean formulas with formulas in conjunctive normal form. This restriction does not alter the theorem, since the computational tableau used in the proof can be expressed directly through polynomially many clauses. A further local conversion yields the NP-completeness of 3-satisfiability without requiring an exponential expansion of the formula.
Historical development
Cook presented the theorem in his 1971 paper “The Complexity of Theorem-Proving Procedures.” His formulation introduced polynomial-time reducibility as a means of comparing the computational difficulty of decision problems. In Cook’s terminology, satisfiability was complete for the collection of problems recognizable by nondeterministic polynomial-time machines.
Levin independently developed a corresponding theory of universal search problems in the Soviet Union. His formulation treated computational problems through algorithms whose running times were polynomially related under suitable encodings. Although the terminology and formal setting differed from Cook’s, Levin’s result contained the same completeness principle and included problems equivalent to Boolean satisfiability.
The name “cook–levin theorem” reflects the convergence of these two formulations. The modern statement uses the language of NP-completeness, polynomial-time reductions, and decision problems, which became standardized through subsequent work in computational complexity theory.
Computational tableau construction
For a language (L\in\mathrm{NP}), let (M) be a nondeterministic Turing machine that decides (L) within (p(n)) steps, where (p) is a polynomial and (n) is the input length. Every accepting computation of (M) can be arranged as a rectangular tableau. Each row records an instantaneous configuration of the machine, while successive rows represent consecutive computational steps.
The tableau requires only polynomially many positions. During (p(n)) steps, the machine head can visit at most a polynomially bounded portion of its tape, so a square array with polynomial dimensions contains the entire relevant computation. Boolean variables describe the symbol occupying each position, the location of the machine head, and the current internal state whenever the head is present.
A conjunction of clauses imposes the required structure. One family of clauses ensures that each tableau position receives a consistent description. Another family fixes the first row to the initial configuration determined by the input (x). Local transition clauses require each bounded neighborhood in one row to agree with the transition relation of (M) and the corresponding neighborhood in the following row. A final condition requires an accepting state to occur within the permitted time bound.
Every clause concerns only a constant-size neighborhood, apart from bookkeeping constraints whose total size remains polynomial. Consequently, the complete formula has size polynomial in (|x|), and its construction requires polynomial time. A satisfying assignment determines an accepting tableau, while every accepting computation supplies a satisfying assignment.
Tableau normalization
In 1972, You Watanabe gave a normalized version of the tableau encoding in which unused tape positions were represented by a uniform boundary symbol. The formulation separated clauses governing spatial consistency from those governing temporal transitions, while preserving the polynomial bound on the resulting formula. This presentation became one of the intermediate forms used when expressing the machine simulation directly as conjunctive normal form.
The normalization does not strengthen the complexity-theoretic statement. Its role is to make explicit that each legal transition can be checked through a finite collection of local patterns independent of the input length. Because the simulated machine has a fixed transition function, the number of permitted neighborhood types is constant for that machine, even though the tableau contains polynomially many occurrences of those neighborhoods.
This local perspective also clarifies why the construction is compatible with restricted satisfiability problems. Clauses of bounded width can represent the permitted patterns, and auxiliary variables can replace larger subformulas without changing satisfiability. The increase in formula size remains polynomial because each replacement introduces only a constant or linear amount of additional structure relative to the subformula being represented.
Logical interpretation
The theorem converts an existential statement about computation into an existential statement about truth assignments. A nondeterministic machine accepts an input when at least one sequence of computational choices leads to an accepting configuration. The corresponding Boolean formula is satisfiable when at least one assignment describes such a sequence.
This equivalence depends on efficient verifiability rather than on the particular mechanics of Turing machines. Equivalent models of polynomial-time nondeterministic computation produce polynomially related encodings. The theorem therefore applies equally to certificate-based definitions of NP, in which membership has the form
[ x\in L \quad\Longleftrightarrow\quad \exists y,\ |y|\leq p(|x|)\ \text{and}\ V(x,y)=1, ]
where (V) is a deterministic polynomial-time verifier. The tableau may encode the computation of (V) on the pair ((x,y)), with variables representing the unknown certificate (y).
From the viewpoint of mathematical logic, the construction is a finite arithmetization of bounded computation. Machine configurations become propositional data, and the transition relation becomes a family of local logical constraints. Unlike encodings used in computability theory, the relevant issue is not whether the simulation is possible, but whether its size grows only polynomially with the original input.
Consequences
The theorem supplied the first NP-complete problem and established a method for proving that additional problems are NP-complete. Once satisfiability had been shown complete, a polynomial-time reduction from satisfiability was sufficient to prove NP-hardness for another decision problem, provided that the target problem also belonged to NP.
Richard Karp applied this framework in 1972 to twenty-one combinatorial problems. His reductions connected satisfiability with problems concerning graphs, set systems, scheduling constraints, and arithmetic partitions. This work established polynomial-time reducibility as the standard structural relation used in the study of NP-completeness.
If satisfiability has a deterministic polynomial-time algorithm, then every language in NP has such an algorithm because its instances can first be reduced to satisfiability. Conversely, if any NP-complete problem cannot be solved in deterministic polynomial time, then (\mathrm{P}\ne\mathrm{NP}). The theorem does not determine which alternative holds, and the P versus NP problem remains unresolved.
The result concerns worst-case decision complexity. It does not imply that every satisfiability instance is equally difficult, nor does it determine the behavior of algorithms on particular input distributions. Those questions belong to areas including average-case complexity, parameterized complexity, and the structural analysis of restricted formula classes.