Communications of the ACM
Cook-Levin: The Ugly Underbelly is Good for Us
I tell my computer science students that we go through proofs not to show WHAT is true, but WHY it's true. During an interesting consultation with a graduate student, who wanted to know whether I proved the Cook-Levin Theorem when I taught that result in the Foundations of Computing class, I said that I had, indeed, and that every teacher should. As is the human predilection, I became ever more fully convinced that I was right as I expounded on it.
The textbook in use is Michael Sipser 3rd Edition [Sipser]. In Section 7.4, we see Cook-Levin as Theorem 7.37: SAT is NP-Complete. The easy part is showing that SAT is in NP, but the gloriously laborious step, the nitty-gritty, is showing that every language A in NP is polynomially time reducible to SAT. This involves pages of close reasoning about the Turing Machine N that decides A .
What have we got to work with?—a language A in NP, and therefore, a nondeterministic TM N that decides A in O(nk) time for some k and input w of length n, and therefore, some accepting computation history of the TM for each word w in A. What are we after?—a propositional formula φ that has a satisfying assignment of truth values if and only if N accepts w.
We create a tableau. We hypothesize an arbitrary word w ∈ A, and plant an accepting branch of its computation history (configurations) in rows of that tableau. We subscript each cell of the table, and form variables from the subscripts and the symbols (the components of N) that will participate in the formula φ, which consists of four conjuncts, each derived with persnickety care from the TM on w. The first establishes the symbol contents of the tape cells, given by disjunct clauses of enumerations of the possibilities, and their settings (true or false) by a conjunct of legality clauses. The other main conjuncts comprise one establishing that the first configuration contains the start state, one doing similar for an accepting state, and one verifying the legality of each move according to the TM's transitions. For that last, we define a window, a frame of six before-and-after tape cells, constructed in excruciating detail, that can be compared to the possible legal transitions of N. And so on... These four conjuncts come together as the φ. Important and subtle point for students: The fact that φ has a satisfying assignment is known by the construction of the first conjunct, although the satisfying assignment itself cannot be constructed since we do not know N or w.
How painful is this?... is a pointless question. We have arrived at the SAT formula φ. Now we calculate the complexity measure of each part, each shown to be polynomial, with their sum therefore also polynomial. Therefore, A ∈ NP. Important and subtle point for students: We have shown this for every lanaguge A in NP, by ignoring any particulars of A and ignoring any particulars of the string w, that is, without loss of generality.
Why should we go to all this trouble, and drag our students through it? Because it shows, indispensably, profoundly, and distinctively, the nature of computability. Here is a Turing Machine, which consists of sets (finite!), supplying givens (definitions!) that provide the (exact!) tools necessary to reach the conclusion. That's all there is. Proofs of other theorems can unveil the same picture, cultivate the same appreciation of the TM concept, but this proof of Cook-Levin seems particularly rich in its layers of exposition, drawing newcomers in so deeply that they inhabit the result. (And it could be even more complicated: Notwithstanding the excruciating detail, Sipser forgoes a precise definition of a legal window.) At all points along the way, we observe where we came from, where we're going, the path we're following, and the vehicle we're taking.
There is no essence of a Turing Machine; there is only the Turing Machine itself, in its five-part or seven-part glory (a 7-tuple in Sipser), and in the protocol for its execution, which applies to all TMs in the class induced by the definition. There is no abstraction or generalization. We humans extrapolate and profit from hand-waving, from simplification and analogy, the type of explanation that I have given verbally above. But there is no substitute for the degree of detail required to turn a TM into a SAT formula.
There is no more: There is no result beyond that which can be obtained from using the symbols, states, and transitions on some input string. A Turing Machine proffers no interpretation. There is no less: There is no shortcut, no gloss. Every bit of the components matters—each state, each symbol from the alphabets, and each transition. A Turing Machine proffers no summary.
References
[Sipser] Michael Sipser. 2012. Introduction to the Theory of Computation. Cengage Learning.
Robin K. Hill is a lecturer in the Department of Computer Science and an affiliate of both the Department of Philosophy and Religious Studies and the Wyoming Institute for Humanities Research at the University of Wyoming. She has been a member of ACM since 1978.
No entries found