How does the 'proof' of the Cook-Levin theorem, actually prove the Cook-Levin theorem?

Question

I was wondering if someone could help resolve some issues I have understanding the proof given for the Cook-Levin theorem provided in the Sipser text (3rd edition) – as this proof has truly stumped me.

Having read through this proof numerous times, the only issue I have is that I simply do not understand how it actually proves the statement in question; namely that the resultant Boolean expression is satisfiable if and only if the nondeterministic Turing machine NM running on ‘w’ accepts on at least one of its computation branches. This is because as far as I can tell, you just produce a big Boolean expression that is always satisfiable, even when NM never accepts the input w. For instance, focusing on the ϕ_accept compound proposition as an example, clearly this is always satisfiable (just set one of the xi,j,q-accept Boolean variables to true – even if this never occurs in any of the computation histories of NM) – consequently what is the point of even including ϕ_accept? The same can be said for the other compound propositions.

As far as I can tell, the resultant Boolean expression produced evaluates to true if and only if NM accepts on one of its computation branches – but this is not what the statement in question actually says. To be clear, what I mean here is that after producing the Boolean expression, if you were to examine the computation history table for every single branch of NM’s computation tree and go about binding each of the variables depending on whether they are actually true or false for that specific computation history table, then ϕ would evaluate to false for every single table if NM rejects, but ϕ would evaluate to true for at least one of the computation history tables if NM accepts. But clearly this is not what the proof is saying, since they never talk about variable binding or the procedure just mentioned. Consequently, I am utterly stumped by this proof – any help would be greatly appreciated.

Answer 1

With careful analysis we can ascertain that this reduction works, meaning that the $NM$ accepts $w$ if and only if $\phi$ is satisfiable (falsifying your claim that $\phi$ is satisfiable anyways)

Lets first have a high level overview of the reduction, $NM$ runs in $O(n^k)$ on input $w$, where $\vert w \vert = n$

We have tableau, an $n^k \times n^k$ table of configurations

We wish to produce $\phi$ such that $\phi$ is satisfiable iff $NM$ has an accepting computation on $w$

Now each cell of the tableau indexed bi $i,j$, $Cell[i,j]$, can have only one symbol out of $C = Q \cup \Gamma \cup \{\#\}$, where $Q$ is set of states of $NM$ and $\Gamma$ is the tape alphabet of $NM$

So for position $(i,j)$ and every symbol $s \in C$, we have a variable $x_{i,j,s}$, where $x_{i,j,s} = 1$ means that $Cell[i,j] = s$

Now lets consider $\phi$ which is composed of four parts

$$\large \phi = \phi_{cell} \land \phi_\text{start} \land \phi_\text{move} \land \phi_{accept}$$

$\phi_\text{cell}$ : ensures only one symbol is on for each $(i,j)$ position, so each cell can have only one symbol

$\phi_\text{start}$ : ensures that the first row of the table is the starting configuration of $NM$ on w

$\phi_\text{move}$ : ensures that all windows in tableau are legal

$\phi_\text{accept}$: ensures that an accepting configuration occurs in the tableau

If we think carefully, the only way to satisfy all of these is to have an accepting computation of $NM$ on $w$

You proposed "cheating", by simply letting some variable $x_{i,j,q_{accepts}}$ be true hence $\phi_{accept}$ would be true, but think again, $\phi_\text{cell}$ would require $Cell[i,j]$ to be $q_\text{accept}$, and if this can not be yielded in an accepting computation, then $\phi_\text{move}$ would be false since you have made an illegal move

You may fool one of the sub-$\phi$s, but you would get caught by another, the only way to satisfy all $\phi_{cell},\phi_\text{start},\phi_\text{move},\phi_{accept}$ and hence satisfy $\phi$ is through the existence of an accepting computation

Hopefully by now, you can see that if $NM$ accepts $w$, there there is some accepting computation, and by turning the corresponding variables on we have a satisfying assignment for $\phi$, also if we have a satisfying assignment we can produce a polynomial size accepting tableau for $NM$