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.
- qij: true if confi is in state j.
- hik: true if the head in confi is at location k.
- tikr: true if the tape cell in location k of confi has element r.
- Every configuration has exactly one state, head location and each tape cell has one element.
- conf0 is the initial configuration.
- confm is accepting.
- For each i≤m, confi+1 follows from confi in one step.
Each configuration in at least one state. For each i we have
t0ixi for i≤n
t0ib for i>n
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).