### Abstract

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.

### License

BSD License

### Topics

- Computer science/Automata and formal languages
- Logic/Computability

### 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

- Basics
- Combinations
- Elementary
- Memorizing
- Composing
- Arithmetic
- Lists_Lists
- Two_Four_Symbols
- Symbol_Ops
- Wellformed
- NP
- Satisfiability
- Oblivious
- Oblivious_Polynomial
- Oblivious_2_Tape
- Reducing
- Aux_TM_Reducing
- Sat_TM_CNF
- Reduction_TM

## Cite

×

Cook_Levin-AFP

    @article{Cook_Levin-AFP,
      author  = {Frank J. Balbach},
      title   = {The Cook-Levin theorem},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Cook_Levin.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Jan 10, 2023 : Isabelle2022