I'm trying to understand the Cook-Levin theorem proof, as it attempts to create a polynomial-time reduction from any NP problem to SAT (as presented in the book by Michael Sipser).

Most requirements are absolutely clear, but I don't understand why the $\phi_{cell}$ formula is required.

Of course, a tableau with improper values, such that fails $\phi_{cell}$, is broken and therefore will not "translate" correctly to the original NP problem on the other side of the reduction. We can easily "break" a tablaue by putting a $q_{accept}$ somewhere where it shouldn't, and the machine's language will change.

But I seem to miss something basic. A reduction says that if A reduces to B, then for each $w\in\Sigma^* $, $w\in A$ iff $f(w)\in B$.

The $f(w)$ part may be the "broken" tableau, but can we really call it $f(w)$? After all, such broken tableaus are never in the image of $f$.

So, why do we care about them?

  • $\begingroup$ Can you give a self-contained description of what the $\phi_\text{cell}$ formula is? I'm familiar with the Cook-Levin proof but I don't know the specific notation or setup used by Sipser, so it would help if you could edit the question to make it self-contained. $\endgroup$
    – D.W.
    May 22, 2017 at 0:48

2 Answers 2


We are building a reduction from problem Q (some problem in NP) to SAT. To do that, we construct a function $f$ that maps an instance of Q to an instance of SAT. In other words, if $w$ is an instance of Q, then $f(w)$ is a formula in CNF form. (Recall that SAT is a decision problem whose instances are CNF formulas.) Let's call that formula $\varphi$. We'll remember that $\varphi$ depends on $w$.

What is the formula $\varphi$? A formula is something that takes any assignment $x$ and assigns a truth value to it, namely $\varphi(x)$. The way the reduction works, we interpret $x$ as a tableau, and $\varphi$ is defined so that $\varphi(x)$ will be true if $x$ is a valid tableau for the input $w$ (a valid computation of a non-deterministic Turing machine for problem $Q$ when run on input $w$).

So, $f(w)$ is not the tableau itself. $f(w)$ is a formula that accepts valid tableaus.

Then, once we have defined $f$ (i.e., $\varphi$), we prove the following property: $\varphi$ will have a satisfying assignment if and only if $w$ is a yes-instance for problem Q.

For this to work out, the formula needs to include terms that ensure that any satisfying assignment to $\varphi$ is a valid tableau. If you left that part out, you wouldn't be able to prove the property mentioned above, so $f$ wouldn't be a correct reduction.


...but I don't understand why the $\phi_{cell}$ formula is required.

The tableau for $N$ in the Sipser's proof represents a single branch of the computation of $N$. The formula $\phi_{cell} \wedge \phi_{start} \wedge \phi_{move} \wedge \phi_{accept}$ in fact kind of seeks for a branch that leads to an accept state. It is true (there is a true-assignment of the variables of this formula) if and only if there is a computation branch that accepts the input.

The proof introduces one variable $x_{i,j,s}$ for each tape cell $cell[i,j]$ so that $x_{i,j,s}$ is true if and only if $cell[i,j] = s$, that is, $cell[i,j]$ contains the symbol $s$.

Now, the idea behind using $\phi_{cell}$ is to require each cell during computation contain only and only a single symbol (you cannot write two different symbols on a cell at the same time), and contain at least one symbol of the alphabet.

But I don't understand what you exactly confused about the reduction. The proof is about how an arbitrary $NP$ decision problem $A$ can be converted to the corresponding $SAT$ problem by generating a formula $\phi_{cell} \wedge \phi_{start} \wedge \phi_{move} \wedge \phi_{accept}$ which is satisfied if only if $A$ has output $yes$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.