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