Flaw in Cook's Theorem Proof: A Critical Analysis of the SAT Reduction

[gnome]

OK, that was just to get your attention. I'm not really challenging the NP-completeness of SAT.

And maybe I'd be going too far even just claiming to have found a flaw in one of the most widely cited proofs of Cook's Theorem. So let's just assume that I'm wrong, and someone please show me why.

The proof described in chapter 2 of Garey & Johnson, "Computers and Intractibility", involves a reduction of all the languages in NP to SAT by defining an NDTM M, specified by $\Gamma, \Sigma, b, Q , q_0, q_Y, q_N, \text{and}\; \delta$, such that establishing membership of a string x in some language L $\in$ NP is equivalent to finding a satisfying truth assignment to a CNF formula. (OK I'm probably grossly oversimplifying, but you know what I mean.)

To accomplish this, the formula will be built up from 3 types of variables, specifically:
$$\begin{array}{ll}\mbox{Variable} &\mbox{Meaning}\\ Q[i,k] &\mbox{At time i, M is in state}\, q_k\\ H[i,j] &\mbox{At time i, the read-write head}\\ &\mbox{ is scanning tape square j}\\ S[i,j,k] &\mbox{At time i, the contents of}\\ &\mbox{tape square j is symbol}\, s_k\end{array}$$

These variables are placed into six groups of clauses with the intended result that a truth assignment on the variables that satisfies the CNF formula will occur if and only if the NDTM M halts in its accepting state in polynomial time. i.e. (formula is satisfied) $\equiv$ (x $\in$ L).

The clause groups are:
$$\begin{array}{ll}\mbox{Clause group} \quad &\mbox{restriction imposed}\\ G1 &\mbox{At each time i, M is in exactly one state.}\\ G2 &\mbox{At each time i, the read-write head is scanning}\\ &\mbox{exactly one tape square.}\\ G3 &\mbox{At each time i, each tape square contains}\\ &\mbox{exactly one symbol from}\, \Gamma.\\ G4 &\mbox{At time 0, the computation is in the initial}\\ &\mbox{configuration of its checking stage for input x.}\\ G5 &\mbox{By time p(n), M has entered state} \, q_Y\\ &\mbox{and hence has accepted x.}\\ G6 &\mbox{For each time i,} \, 0 \leq i \leq p(n) \,\mbox{ the configuration}\\ &\mbox{of M at time i+1 follows by a single}\\ &\mbox{application of the transition function} \, \delta\\ &\mbox{from the configuration at time i.}\end{array}$$

Actually, Group 6 is divided into 2 sub-groups. the first sub-group is to guarantee that if the read-write head is not scanning tape square j at time i, then the symbol in square j does not change between times i and i+1. The other subgroup of G6 guarantees that the changes from one configuration to the next are in accord with the transition function $\delta$ for M.

Now, to have a valid reduction, it must be so that a machine that correctly recognizes L must correspond to a truth assignment that satisfies all of these clauses. And conversely, there must not be a truth assignment that satisfies all of the clauses but is not a valid, accepting computation of L. However, I don't think that the clauses supplied are sufficient to accomplish this. My problem is with the first subgroup of Group 6. The clauses in that subgroup are of the form:

$$\{\overline{S[i,j,l]}, H[i,j], S[i+1,j,l]\}$$

To reiterate, that was supposed to ensure that the contents of tape square j can change from time i to time i+1 only if the read-write head was looking at tape square j at time i.

Suppose we have this truth assignment for some clause $c_a$:
$$\begin{array}{ll}\text{True} &\overline{S[i,j,l]}\\ \text{False} &H[i,j]\\ \text{True} &S[i+1,j,l]}\end{array}$$

This means that at time i the read-write head is not scanning square j, and also at time i the symbol in square j is not $s_l$, but at time i+1 square j does contain symbol $s_l$. Since the clause is a disjunction, it is true. And therefore the entire formula (a conjunction of these disjunctive clauses) may be satisfied. But clearly this does not represent a valid computation of L, right?

Then the whole proof is out the window, unless someone can come up with some clause or group of clauses (remember they must be disjunctions) that fulfill the mission of the first subgroup of G6. I haven't been able to. Can you?

 

[gnome]

PS: Why does every textbook present it's own proof of Cook's Theorem? Why don't they show us Cook's proof?

 

[matt grime]

Without wishhing to sound lazy, what on Earth is SAT? I can't be arsed to look it up, and I suspect few others can either. But, hey, you want to introduce unexplained acronyms, ans refer to a book that maybe 2 other readers here even know exists, go right ahead.

Incidentally, do you even know Cook proved this? Just cos it has his name on it doesn't mean he even knows the statement of the theorem (like everyone else here). As Brauer once said in a seminar to the speaker: would you mind telling me what Brauer's trick is?

 

[NateTG]

Without wishhing to sound lazy, what on Earth is SAT? I can't be arsed to look it up, and I suspect few others can either. But, hey, you want to introduce unexplained acronyms, ans refer to a book that maybe 2 other readers here even know exists, go right ahead.

In the context of NP-completeness, SAT is the satsifyability problem. And 3-SAT is probably what he's referring to. The satsifyability problem is to find truth values for variables $a_1,a_2...a_n$ i.e. (T or F) so that a particular logical expression is true. 3-SAT restricts this to logical expressions of a particular form.

 

[gnome]

Sorry, matt. I guess I've just seen it pop up so many times in the past year or so that I just assume everyone knows what it is. I still think that's a fair assumption for just about anyone who's done postgrad work in computer science and I kind of thought, maybe unfairly, that would also be the case for people doing advanced work in math.

Anyway, yeah, it's the Satisfiability problem; Michael Sipser defines it very nicely as:
$$SAT = \{\phi\,|\,\phi \,\mbox{is a satisfiable Boolean formula}\}$$
Cook's Theorem, according to what I've read, is that Satisfiability is NP-complete. And as to whether Cook proved it, I don't know, but I believe that it's named for him because he was supposedly the first one to prove that any particular problem is NP-complete (which I guess made him some kind of hero to all the algorithms folks who needed something provable to point to as the reason why they couldn't find an efficient solution to some problem or other).

Nate, I didn't mean 3-SAT. 3-SAT is SAT with the limitation that the Boolean formula in question is a conjunction of disjunctions where each disjunction consists of exactly 3 distinct literals (although some of the definitions I've seen omit "distinct", and others just say 3 variables). SAT (the general form) doesn't specify Conjunctive Normal Form, but every proof I've seen puts it in CNF. I'm not 100% sure why; I think because in that form it's most amenable to algorithmic solution.

As I'm writing this it occurs to me that someone else (can't remember who, maybe Chomsky?) has a theorem that says that any Boolean formula can be put into CNF. Maybe that's the solution to my (or this author's) problem. Just come up with any kind of clauses that accomplish G6's job, and then figure out how to transform them into CNF. Maybe.

 

[master_coda]

Then the whole proof is out the window, unless someone can come up with some clause or group of clauses (remember they must be disjunctions) that fulfill the mission of the first subgroup of G6. I haven't been able to. Can you?

Couldn't you just use both

$$\{\overline{S[i,j,l]}, H[i,j], S[i+1,j,l]\}$$

and

$$\{S[i,j,l], H[i,j], \overline{S[i+1,j,l]}\}$$

or perhaps I'm misunderstanding what you're trying to find.

PS: Why does every textbook present it's own proof of Cook's Theorem? Why don't they show us Cook's proof?

In my experience, most textbook authors will modify the proof's they present to try and supply a consistent style. The original proof written by Cook wasn't really written to be directly included in a textbook.

 

[matt grime]

As some one finishing their postgrad in maths and with a postdoc lined up, can I vouch that we don't all know the intricacies of algorithmic results or computer science (I wouldn't expect you to be able to give me an example of a functor diagram that shows that rigidification cannot be dropped when considering homotopy colimits of based spaces). In fact I can't think of any mathematician I know who'd have understood that - and there are only, what, 6-10 readers of this forum who have more than undergrad maths (many more have postgrad other stuff, before they get uppity). Anyway, it's good that there are more difficult topics being raised, sadly (despite guessing NF was normal form) I can't help you except to say that it is entirely conceivable that Cook didn't prove Cook's Theorem, and if he did the original proof would be, to echo Mastercoda, highly unlikely to be suitable for book presentation - proofs go through refinement processes as people look over them and realize that they can be improved, or that certain stages are not important, or perhaps that there's no need to separate into so many cases.

 

[Hurkyl]

Just come up with any kind of clauses that accomplish G6's job, and then figure out how to transform them into CNF. Maybe.

That's what I would do. Of course, unless you're trying to show 3-SAT is NP-complete, I wouldn't bother transforming to CNF. We know it can be done, but we don't need to know exactly how it looks.

 

[gnome]

Couldn't you just use both

$$\{\overline{S[i,j,l]}, H[i,j], S[i+1,j,l]\}$$

and

$$\{S[i,j,l], H[i,j], \overline{S[i+1,j,l]}\}$$

or perhaps I'm misunderstanding what you're trying to find.

That's it! Many thanks.

 

[gnome]

In fact I can't think of any mathematician I know who'd have understood that ...

Were you referring to my post or to your statement about based spaces?

 

[John136]

about 3SAT

Hi gnome,

I just wonder if you insist on your opinion about the proof of 3SAT ?

Looking forward to hearing from you !

John