Complexity Dojo/Cook-Levin Theorem

From Complexity Zoo
Jump to: navigation, search

Main Zoo - Complexity Garden - Zoo Glossary - Zoo References - Chris' Complexity Dojo


Major Theorems: Cook-Levin - Savitch's - Ladner's - Blum Speedup - Impagliazzo-Widgerson - Toda's - Natural Proofs

Proof Techniques: Diagonalization


The Cook-Levin Theorem shows that any problem in NP is reducible to SAT in polynomial time. Thus, SAT is at least as hard as every other problem in NP (we call this property NP-hardness). Being in NP itself, this implies that SAT somehow encapsulates why problems in NP are hard. It is important enough that we say that SAT is NP-complete.

The Cook-Levin Theorem also lets us show that other problems are NP-complete by reducing SAT to them in polynomial time, since polynomials are closed under composition. Thus, the theorem acts as a starting point for further study of NP-completeness.

There are actually many versions of the proof of Cook-Levin Theorem. Some versions, such as the one presented by [Pap94] reduce NP problems to the Circuit-SAT problem (a variant of SAT), then use as a lemma that Circuit-SAT is reducible to SAT. In doing so, they prove a slightly stronger result that Circuit-SAT is also NP-complete. Other versions of the proof, such as the one given by Wikipedia, employ a gaggle of variables to represent the NP machine being reduced to SAT. In either case, however, what remains is that the satisfiablity instance constructed by the proof simulates an NP machine, and thus solving it gives you the ability to solve arbitrary NP problems for which an NP machine has been devised (as opposed to those problems that we place in NP non-constructively).

Moreover, most (if not every) version of the proof relies on the locality of a Turing machine. That is, we shall rely upon the fact that since the transition function for a Turing machine depends only on the symbols under each read head and the machine state, we can describe the Turing machine as the combination of a series of local descriptions.

This is a commonly enough covered theorem that we shall not give a proof here, but rather shall be content to direct the reader to one of the proofs given elsewhere (please expand this list if you find a good proof somewhere):

Personal tools
Namespaces

Variants
Actions
Navigation
Toolbox