patternMinor
Cook-Levin theorem proof's requirement of $\phi_{cell}$
Viewed 0 times
cellcookrequirementtheoremlevinphi_proof
Problem
I'm trying to understand the Cook-Levin theorem proof, as it attempts to create a polynomial-time reduction from any
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?
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?
Solution
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.
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.
Context
StackExchange Computer Science Q#75638, answer score: 2
Revisions (0)
No revisions yet.