Cook–Levin Theorem

The **Cook–Levin theorem** states that the Boolean satisfiability problem (SAT) is NP-complete — it is in NP and every problem in NP reduces to it via a polynomial-time reduction. ## Who and when - **Stephen Cook** presented it in 'The complexity of theorem proving procedures' at the 1971 ACM Symposium on Theory of Computing (STOC). - **Leonid Levin** developed equivalent results independently in the USSR, published in 'Universal search problems' (1973). - **Richard Karp** (1972, 'Reducibility among combinatorial problems') used polynomial-time many-one reductions to show 21 further problems are NP-complete, demonstrating the theory's reach. - Cook and Karp both received Turing Awards for this line of work. ## The proof idea The proof encodes the computation of an arbitrary nondeterministic Turing machine (running in polynomial time) as a Boolean formula. The formula is constructed so that it is **satisfiable if and only if the machine has an accepting computation** on the given input. Since any NP problem is, by definition, decided by such a machine, this generically reduces every NP problem to SAT. ## Why it matters The theorem established NP-completeness as a meaningful, non-empty concept and gave a 'first' complete problem from which all others could be proven complete by reduction. It also shows that a polynomial-time algorithm for SAT would imply P = NP, tying one concrete logic problem to the central open question of computer science.