The Cook-Levin theorem

Frank J. Balbach 📧

January 8, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


The Cook-Levin theorem states that deciding the satisfiability of Boolean formulas in conjunctive normal form is $\mathcal{NP}$-complete. This entry formalizes a proof of this theorem based on the textbook Computational Complexity: A Modern Approach by Arora and Barak. It contains definitions of deterministic multi-tape Turing machines, the complexity classes $\mathcal{P}$ and $\mathcal{NP}$, polynomial-time many-one reduction, and the decision problem $\mathtt{SAT}$. For the $\mathcal{NP}$-hardness of $\mathtt{SAT}$, the proof first shows that every polynomial-time computation can be performed by a two-tape oblivious Turing machine. An $\mathcal{NP}$ problem can then be reduced to $\mathtt{SAT}$ by a polynomial-time Turing machine that encodes computations of the problem's oblivious two-tape verifier Turing machine as formulas in conjunctive normal form.


BSD License


Related publications

  • Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2006.
  • Stephen A. Cook. The complexity of theorem-proving procedures. Proceedings of the third annual ACM symposium on Theory of computing, 1971.
  • L. A. Levin. Universal sequential search problems. Problems of Information Transmission, 9(3):265–266, 1973.

Session Cook_Levin