The Cook-Levin theorem

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.