TheoremProved

Cook–Levin theorem

Statement

The Boolean satisfiability problem (SAT) is NP-complete: SAT is in NP, and every language in NP is polynomial-time reducible to SAT. Consequently, if SAT can be solved in polynomial time, then P = NP.

Why is it true?

NP problems are exactly those whose proposed solutions can be checked quickly, even if finding them might be hard. SAT — deciding whether a Boolean formula can be made true — looks like just one specific puzzle among many, but it turns out to be a 'universal translator': the computation of any polynomial-time verifier checking any candidate solution to any NP problem can be encoded, step by step, as a Boolean formula that is satisfiable exactly when a valid solution exists. So SAT is at least as hard as every problem in NP.

Proof sketch

Given any language $L \in \mathrm{NP}$ , fix a polynomial-time verifier's Turing machine and a polynomial bound on running time. Encode the machine's entire computation on an input of length $n$ as a large grid of Boolean variables recording, for every time step and tape cell, the symbol written, head position, and machine state. Clauses enforce: exactly one symbol/state per cell/step, correct initial configuration, correct transition rule between consecutive time steps, and an accepting state reached by the end. This conjunction of clauses is satisfiable exactly when there is an accepting computation, i.e. exactly when the input is in $L$ , and its size is polynomial in $n$ , giving a polynomial-time reduction from $L$ to SAT.

Stated by

Stephen Cook

Proved by

proved 1971Stephen Cook

Topics that use this theorem

Computational complexity: P and NP

Related theorems

Undecidability of the halting problem

Step-by-step proofs

No step-by-step proof yet for this theorem.

References

Stephen A. Cook (1971). The complexity of theorem-proving procedures
Michael R. Garey, David S. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness