CSC 341: May 2, 2007
From CSWiki
Instructor's notes for the class session
The problem SAT is polynomially verifiable. A polynomial-time deterministic Turing machine can confirm that a given Boolean expression is satisfiable if it is also given, as a certificate, a satisfying assignment of Boolean values to the variables occurring in the expression (that is, an assignment under which the given Boolean expression is true).
The hard part of the proof of the Cook-Levin theorem is to demonstrate that every polynomially verifiable language is polynomial-time reducible to SAT. The proof is a reduction via computational history, using the general approach described in section 5.1 (pages 192 and 193) of the textbook.
Let A be any polynomially verifiable language. By Theorem 7.20, there is a nondeterministic polynomial-time Turing machine N that recognizes A. By Corollary 7.22, there is some positive integer k such that the running-time function of N is O(nk), so that there is some order-k polynomial f that bounds that running-time function.
For any input of length n, then, we can store a complete trace of any computation that N can make in processing that input in a tableau -- an array of f(n) + 1 rows and f(n) + 4 columns, each element of which is either one symbol from N's tape alphabet, the name of one of N's states, or an end-marker symbol. We can regard each row of a tableau as a possible configuration of N -- the first row as the initial configuration for the given input, and each subsequent row as a possible successor to the preceding one. We may need f(n) + 1 rows to hold the initial configuration and the configuration after each of the f(n) transitions that N might make before reaching the accept state or the reject state.
For each row i and each column j of the tableau, and each s that is either a symbol in N's tape alphabet, the name of one of N's states, or the end-marker, we posit a Boolean variable xi,j,s, which will be true if, and only if, s is the element at row i, column j of the tableau.
We'll require an end-marker to occur at the beginning and end of each row, so that we can test whether N's read-write head is on the first or last cell represented in the configuration. It is sufficient to provide f(n) + 4 tableau elements to represent any configuration that can be reached during the computation: Two for the end-markers, one for the state, and f(n) + 1 for the tape cells. (Even if N's read-write head moves rightwards on every transition, it cannot move more than f(n) positions rightwards in f(n) steps.)
Now we're ready to describe how to construct a Boolean expression that is satisfiable if, and only if, the computational history represented in the tableau ends (in its last row) with an accepting configuration of N.
First, we need a subexpression that ensures that each cell of the tableau is occupied by one and only one symbol from N's tape alphabet, name of one of N's states, or end-marker. For each row i and column j, we construct one clause that is a disjunction of all the Boolean variables xi,j,s (for all the possible values of s; this ensures that every cell contains at least one element. There will be O(f2(n)) such clauses, each containing a number of literals that is independent of n, so the total length of this set of clauses is O(f2(n)). In addition, for each row i, column j, and possible elements s and t, there will be a clause that is the disjunction of 
and 
; this ensures that no cell contains more than one element. Again, there will be O(f2(n)), each with two literals, so the total length of this set of clauses is again O(f2(n)).
Next, we need a subexpression that ensures that the top row of the tableau contains an initial configuration of N. Specifying the contents of each cell in that row requires f(n) + 4 clauses, each containing a single literal. So the total length of this set of clauses is O(f(n)).
Next, we need a subexpression that ensures that each row of the tableau differs from the one above it only in the vicinity of the read-write head (or not at all, if N has reached qaccept or qreject), and that any changes that occur in the vicinity of the read-write head are consistent with a transition that is permitted by N's transition function. We do this by considering each two-cell-by-three-cell subarray of the tableau separately and confirming that the contents of such a subarray match one of a finite, fixed number of legal patterns. This confirmation requires 6m separate clauses, where m is the number of legal patterns, for each of the O(f2(n)) two-cell-by-three-cell subarrays. Each clause will be a disjunction of k unnegated literals. Since m is independent of the n, the length of this subexpression is again O(f2(n)).
Finally, we need a subexpression checking for the presence of qaccept in the bottom row of the tableau. This can be done in a single clause in which the disjuncts are unnegated literals, one for each cell of the bottom row. The length of this subexpression is O(f(n)).
Adding, we find that the length of the entire expression formed by conjoining all of the clauses is O(f2(n)). Since f itself is O(nk), the length of the entire expression is O(n2k), which is a polynomial. So we can construct it in polynomial time. So our preprocessor can convert the question of whether N accepts a particular input into a satisfiability question in polynomial time. So, if SAT is decidable in polynomial time, so is A.
Study question
- The preceding construction doesn't work correctly when the running time of the nondeterministic decider is sublinear -- that is, when its running-time function is o(n) (note: little o, as in Definition 7.5), because the computation history of the nondeterministic decider on sufficiently large inputs may not be fully representable in the tableaus as I have designed them above. What changes in the design of the tableau would be need to make it work in these cases as well? Can these changes be made without losing the polynomial-time reducibility of the preprocessor?
Proposed Solutions
- (discussed in class, I believe credit is due to CM Lubinski): All that needs to be done is to make the length (and width) of the tableau the max of the running time of the machine and the length of the machine's input. Now, the construction of the tableau should work in all cases.
