Sipser's proof of NP-completeness of SAT  I just need some help with the Cook-Levin theorem (SAT is NP-complete).
The proof of this theorem is not so clear to me.
I use Sipser's book "Introduction to the Theory of Computation". 
Up to this proof, everything else seems very clear and obvious; therefore I chose this book. The proof is on the page 277.
I can't understand the concept of the tableau from the very beggining .
In particular,


*

*every row in tablea presents branch with states if corresponding nodes in TM?

*what is the idea of window stands for ?
May be there is any simplified version, you know of?
Thanks!

Thanks for great explanation!
I would like to ask you few more questions
the idea of tableau is clear
the idea of cell is clear 
but I still have a problem with designing $\phi$ (correspond boolean expression to input $\omega$)
Now we design $\phi$ so that a satisfing assignment to the variables does correspond to an accepting tableau for N on $\omega$. The formula for $\phi$ is the AND of four parts $\phi_{cell}\wedge\phi_{start}\wedge\phi_{move}\wedge\phi_{accept} $ (how can this construction describe $\phi$?) . We describe each part in turn.
As we mentioned previously, tunrning variable $x_{i,j,s}$ on corresponds to placing symbol $s$ in $cell[i,j]$  The first thing we must guarantee in order to obtain a correspondence beetwen  an assignment and a tableau is that the assignment turns on exactly one variable for each cell. Formula $\phi_{cell}$ ensures this requirments by expressing it in terms of Boolean operations
$$\phi_{cell} = \underset{1\leqslant i, j\leqslant n^{k}}{\wedge }\left [  \left (  \underset {s\epsilon C}{\wedge} x_{x,j,s} \right ) \wedge \left (\underset{\underset{s\neq t}{s,t\epsilon C}}{\wedge}  \left ( \overline{x_{i,j,s}} \vee \overline{x_{i,j,t}} \right ) \right ) \right ]$$
Why $\phi_{cell}$ has a above equation?
Thanks! 
 A: I'm using a second answer to answer your newly added question. You made a little mistake, the cell formula should be the following: 
$$\phi_{cell} = \underset{1\leqslant i, j\leqslant n^{k}}{\wedge }\left [  \left (  \underset {s\epsilon C}{\vee} x_{i,j,s} \right ) \wedge \left (\underset{\underset{s\neq t}{s,t\epsilon C}}{\wedge}  \left ( \overline{x_{i,j,s}} \vee \overline{x_{i,j,t}} \right ) \right ) \right ]$$
As you said, the variable $x_{i,j,s}$ represents the symbol s in cell[i,j], so it should be true if and only iff cell[i,j] contains the symbol $s$. Let's analyse the cell formula properly. It exists out of 3 parts:


*

*$\Large\underset {s\epsilon C}{\vee} x_{i,j,s}$ tells that for each fixed $i$ and $j$ there should be atleast one symbol $s$ in cell[i,j].

*$\large\underset{\underset{s\neq t}{s,t\epsilon C}}{\wedge}  \left ( \overline{x_{i,j,s}} \vee \overline{x_{i,j,t}} \right )$ says that, for each distinct pair of symbols $s$ and $t$: $\large x_{i,j,s}$ and $\large x_{i,j,t}$ cannot both be true at the same time. This represents that a cell cannot have more then one symbol.


Combining both points tells us that for each fixed $i$ and $j$ there has to be exactly one symbol $s$ ( NOT MORE AND NOT LESS) so that variable $x_{i,j,s} = 1$. More intuitively it tells us that each cell can only contain exactly one symbol. 
Now the only thing left is to analyse is the $\large\underset{1\leqslant i, j\leqslant n^{k}}{\wedge }$ part encapsulating the parts we already analysed. Clearly this part just tells us that the formula has to hold for each cell in the tableau.
I hope this helped.
A: The tableau represents the turing machine its computation.
Each row in the tableau is a snapshot of the Turing machine his computation. I think Sipser calls this a configuration. This configuration contains the Turing machine's tape contents, the current position of the tape and the current state the Turing machine is in.
Now, a whole tableau represents a computation of a Turing machine, where the first row in the tableau is the starting configuration containing the start state and the input. The last row of a tableau is either a rejecting configuration or an accepting configuration.
A deterministic Turing machine has only one tableau for each input, since the computation is deterministic. A nondeterministic Turing machine can have multiple tableaus for a single input, each representing a branch in the nondeterministic machine's computation.
To explain the window in a tableau, you need to think of the Turing machine's transition function. In each step the Turing machine makes, it reads a symbol, moves its tape head and writes a symbol, thus for a tableau to be correct, every window has to be correct according to the transition function. The reason why a window contains 6 cells, is because the computation of a Turing machine is highly local. With highly local we mean that it can only effect a few cells in each computation step. Clearly, if you examine the transition function, you will see that it can only effect the cell where it is currently in, and the cell to the left or the right. 
To make a long story short:
The tableau represents the Turing machine's computation, where each row represents a step in the Turing machine. Obviously, to make sure that the computation is correct, you have to check each window according to the transition function, else the tableau does not represent a Turing machine his computational steps.
Now, the reason why they use the tableau is: if there is a tableau with an accepting configuration as its last row, the Turing machine accepts the input in the starting configuration of that tableau. Then, they observe that you can find a SAT formula that mimics this tableau. Thus, you have found a formula which is satisfiable if and only if the Turing machine accepts the given input.
