We will show that CNF-SAT
is NP-complete.
Let A be a language in NP accepted by a nondeterministic Turing
machine M. Fix an input x. We will create a 3CNF formula φ that
will be satisfiable if and only if there is a proper
tableau for M and x.

Let m be the running time of M on x. m is bounded by a polynomial in |x| since A is in NP. m is also a bound on the size of the configurations of M(x).

We will create a set of Boolean variables to describe a tableau and a set of clauses that will all be true if and only if the tableau is proper. The variables are as follows.

Each configuration in at least one state. For each i we have

q
Each configuration in at most one state. For each i and possible
states v and w, v≠w

(NOT q
2. Let x=x

q

h

t

t
3. Let a be the accept state. We need only one single variable clause.

q
4. We need two parts. First if the head is not over a tape location
then it should not change.

((NOT h
Now this doesn't look like an OR of literals. We now apply the facts
that P→Q is the same as (NOT P) OR Q and NOT(R AND S) is equivalent to
(NOT R) OR (NOT S) to get

h
At this point none of the formula has been dependent on the machine M.
Our last set of clauses will take care of this. Recall the program of a
Turing machine is a mapping from current state and tape character
under the head to a new state, a possibly new character under the head
and a movement of the tape head one space right or left. A
nondeterministic machine may allow for several of these
possibilities. We add clauses to prevent the wrong operations.

Suppose that the following is NOT a legitimate transition of M: In state j and tape symbol r, will write s, move left and go to state v. We prevent this possibility with the following set of clauses (for all appropriate i and k).

(q
which is equivalent to

(NOT q
We do this for every possible illegitimate transition. Finally we just
need to make sure the head must go one square right or left in each
turn.

(NOT h
Just to note in the above formula we need special care to
handle the boundary conditions (where k is 1 or m) but this is
straightforward.

Let m be the running time of M on x. m is bounded by a polynomial in |x| since A is in NP. m is also a bound on the size of the configurations of M(x).

We will create a set of Boolean variables to describe a tableau and a set of clauses that will all be true if and only if the tableau is proper. The variables are as follows.

- q
_{ij}: true if conf_{i}is in state j. - h
_{ik}: true if the head in conf_{i}is at location k. - t
_{ikr}: true if the tape cell in location k of conf_{i}has element r.

- Every configuration has exactly one state, head location and each tape cell has one element.
- conf
_{0}is the initial configuration. - conf
_{m}is accepting. - For each i≤m, conf
_{i+1}follows from conf_{i}in one step.

Each configuration in at least one state. For each i we have

_{i0}OR q

_{i1}OR ... OR q

_{iu}

_{iv}) OR (NOT q

_{iw})

_{1}...x_{n}, b the blank character and state 0 the initial state. We have the following single variable clauses,_{00}

h

_{01}

t

_{0ixi}for i≤n

t

_{0ib}for i>n

_{ma}

_{ }

_{ik}) AND t

_{ikr})→ t

_{i(k+1)r}

_{ }

_{ik}OR (NOT t

_{ikr}) OR t

_{(i+1)kr}

_{ }

Suppose that the following is NOT a legitimate transition of M: In state j and tape symbol r, will write s, move left and go to state v. We prevent this possibility with the following set of clauses (for all appropriate i and k).

_{ij}AND h

_{ik}AND t

_{ikr})→ NOT(t

_{(i+1)ks}AND h

_{i(k-1)}AND q

_{(i+1)v})

_{ij}) OR (NOT h

_{ik}) OR (NOT t

_{ikr}) OR (NOT t

_{(i+1)ks}) OR (NOT h

_{i(k-1)}) OR (NOT q

_{(i+1)v})

_{ik}) OR h

_{(i+1)(k-1)}OR h

_{(i+1)(k+1)}

_{ }