Cook-Levin theorem proof's requirement of $\phi_{cell}$

Question

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?

Answer 1

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.

Answer 2

...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$.