Editing Cook–Levin theorem (section)

==Proof==
''This proof is based on the one given by {{harvnb|Garey|Johnson|1979|loc=Section 2.6|pp=38–44}}.''

There are two parts to proving that the Boolean satisfiability problem (SAT) is NP-complete. One is to show that SAT is an NP problem. The other is to show that every NP problem can be reduced to an instance of a SAT problem by a [[polynomial-time many-one reduction]].

SAT is in NP because any assignment of Boolean values to Boolean variables that is claimed to satisfy the given expression can be ''verified'' in polynomial time by a deterministic Turing machine. (The statements '''''verifiable''' in polynomial time by a '''deterministic''' Turing machine'' and '''''solvable''' in polynomial time by a '''non-deterministic''' Turing machine'' are equivalent, and the proof can be found in many textbooks, for example Sipser's ''Introduction to the Theory of Computation'', section 7.3., as well as [[NP (complexity)#Equivalence of definitions|in the Wikipedia article on NP]]).

[[File:CookLevinCommDiag svg.svg|thumb|[[Commutative diagram]] showing Cook's reduction of <math>M</math> to SAT. Data sizes and program runtimes are colored in {{color|#cc6600|orange}} and {{color|#006600|green}}, respectively.]]
[[File:CookLevin_svg.svg|thumb|Schematized accepting computation by the machine <math>M</math>.]]
Now suppose that a given problem in NP can be solved by the [[nondeterministic Turing machine]] <math>M = (Q, \Sigma, s, F, \delta)</math>, where <math>Q</math> is the set of states, <math>\Sigma</math> is the alphabet of tape symbols, <math>s \in Q</math> is the initial state, <math>F \subseteq Q</math> is the set of accepting states, and <math>\delta \subseteq ((Q \setminus F) \times \Sigma) \times (Q \times \Sigma \times \{-1, +1\})</math> is the transition relation. Suppose further that <math>M</math> accepts or rejects an instance of the problem after at most <math>p(n)</math> computation steps, where <math>n</math> is the size of the instance and <math>p</math> is a polynomial function.

For each input, <math>I</math>, specify a Boolean expression <math>B</math> that is satisfiable [[if and only if]] the machine <math>M</math> accepts <math>I</math>.

The Boolean expression uses the variables set out in the following table. Here, <math>q \in Q</math> is a machine state, <math>-p(n) \leq i \leq p(n)</math> is a tape position, <math>j \in \Sigma</math> is a tape symbol, and <math>0 \leq k \leq p(n)</math> is the number of a computation step.

{| class="wikitable"
!Variables
!Intended interpretation
!How many?<ref>This column uses the [[big O notation]].</ref>
|-
|<math>T_{i,j,k}</math>
|True if tape cell <math>i</math> contains symbol <math>j</math> at step <math>k</math> of the computation.
|<math>O(p(n)^2)</math>
|-
|<math>H_{i,k}</math>
|True if <math>M</math>'s read/write head is at tape cell <math>i</math> at step <math>k</math> of the computation.
|<math>O(p(n)^2)</math>
|-
|<math>Q_{q,k}</math>
|True if <math>M</math> is in state <math>q</math> at step <math>k</math> of the computation.
|<math>O(p(n))</math>
|}

Define the Boolean expression <math>B</math> to be the [[Logical conjunction|conjunction]] of the sub-expressions in the following table, for all <math>-p(n) \leq i \leq p(n)</math> and <math>0 \leq k \leq p(n)</math>:

{| class="wikitable"
!Expression
!Conditions
!Interpretation
!How many?
|-
|<math>T_{i,j,0}</math>
|Tape cell <math>i</math> initially contains symbol <math>j</math>
|Initial contents of the tape.  For <math>i > n-1</math> and <math>i < 0</math>, outside of the actual input <math>I</math>, the initial symbol is the special default/blank symbol.
|<math>O(p(n))</math>
|-
|<math>Q_{s,0}</math>
| 
|Initial state of <math>M</math>.
|1
|-
|<math>H_{0,0}</math>
| 
|Initial position of read/write head.
|1
|-
|<math>\neg T_{i,j,k} \lor \neg T_{i,j',k}</math>
|<math>j \neq j'</math>
|At most one symbol per tape cell.
|<math>O(p(n)^2)</math>
|-
|<math>\bigvee_{j \in \Sigma} T_{i,j,k}</math>
|
|At least one symbol per tape cell.
|<math>O(p(n)^2)</math>
|-
|<math>T_{i,j,k} \land T_{i,j',k+1} \rightarrow H_{i,k}</math>
|<math>j \neq j'</math>
|Tape remains unchanged unless written by head.
|<math>O(p(n)^2)</math>
|-
|<math>\lnot Q_{q,k} \lor \lnot Q_{q',k}</math>
|<math>q \neq q'</math>
|At most one state at a time.
|<math>O(p(n))</math>
|-
|<math>\bigvee_{q \in Q} Q_{q, k}</math>
|
|At least one state at a time.
|<math>O(p(n))</math>
|-
|<math>\lnot H_{i,k} \lor \lnot H_{i',k}</math>
|<math>i \neq i'</math>
|At most one head position at a time.
|<math>O(p(n)^3)</math>
|-
|<math>\bigvee_{-p(n) \le i \le p(n)} H_{i, k}</math>
|
|At least one head position at a time.
|<math>O(p(n)^2)</math>
|-
|<math>\begin{array}{l}
(H_{i,k} \land Q_{q,k} \land T_{i,\sigma,k}) \to \\
\bigvee_{((q, \sigma), (q', \sigma', d)) \in \delta} (H_{i+d,\ k+1} \land Q_{q',\ k+1} \land T_{i,\ \sigma',\ k+1})
\end{array}</math>
|<math>k < p(n)</math>
|Possible transitions at computation step <math>k</math> when head is at position <math>i</math>.
|<math>O(p(n)^2)</math>
|-
|<math>\bigvee_{0 \le k \le p(n)} \bigvee_{f \in F} Q_{f,k}</math>
|
|Must finish in an accepting state, not later than in step <math>p(n)</math>.
|1
|}

If there is an accepting computation for <math>M</math> on input <math>I</math>, then <math>B</math> is satisfiable by assigning <math>T_{i,j,k}</math>, <math>H_{i,k}</math> and <math>Q_{i,k}</math> their intended interpretations. On the other hand, if <math>B</math> is satisfiable, then there is an accepting computation for <math>M</math> on input <math>I</math> that follows the steps indicated by the assignments to the variables.

There are <math>O(p(n)^2)</math> Boolean variables, each encodable in space <math>O(\log p(n))</math>. The number of clauses is <math>O(p(n)^3)</math><ref>The number of literals in each clause does not depend on <math>n</math>, except for the last table row, which leads to a clause with <math>O(p(n))</math> literals.</ref> so the size of <math>B</math> is <math>O(\log(p(n)) p(n)^3)</math>. Thus the transformation is certainly a polynomial-time many-one reduction, as required.

Only the first table row (<math>T_{i,j,0}</math>) actually depends on the input string <math>I</math>. The remaining lines depend only on the input length <math>n</math> and on the machine <math>M</math>; they formalize a generic computation of <math>M</math> for up to <math>p(n)</math> steps.

The transformation makes extensive use of the polynomial <math>p(n)</math>. As a consequence, the above proof is not [[constructive proof|constructive]]: even if <math>M</math> is known, [[witness (mathematics)|witness]]ing the membership of the given problem in NP, the transformation cannot be effectively computed, unless an upper bound <math>p(n)</math> of <math>M</math>'s time complexity is also known.