{\huge Cook's Theorem}

Another proof of Cook's Theorem \vspace{.5in}

Steve Cook proved three landmark theorems with 1971 dates. The first has been called a ``surprising theorem'': that any deterministic pushdown automaton with two-way input tape can be simulated in linear time by a random-access machine. This implies that string matching can be done in linear time, which inspired Donald Knuth and Vaughan Pratt to find a direct algorithm that removes a dependence on the input alphabet size. This was before they learned that James Morris had found it independently, later than but without knowledge of Cook, and their algorithm is now called KMP. Fast string matching has thousands of applications. Second was his characterization of polynomial time by log-space machines with auxiliary pushdowns, a fact which may yet help for proving lower bounds. Then there was his third result, which appeared at STOC 1971, and was given a ``slif'' (stronger, later, independent form) by Leonid Levin.

Today I want to present a proof of the famous Cook-Levin Theorem that $latex {\mathsf{SAT}}&fg=000000$ is $latex {\mathsf{NP}}&fg=000000$-complete.

I am currently giving a class on complexity theory, and thought this proof might have some advantage over the usual proofs. There are the original tableau-based proofs, the later circuit-based proofs, and variations of them.

The proof here is based on my favorite kind of objects---well one of them---finite automata. They are remarkably powerful and can be used to give a relatively clean proof. At least I believe the proof is clean for students---I would like to hear any thoughts that you all may have about it. It needs no assumption about oblivious tape access patterns, and does not use lots of complex indexing.

So let's take a look at the proof. Here is a Wordle from STOC 1971:

\includegraphics[width=3in]{stoc1971.png}

Introduction

My goal is to try and give a proof of Cook's famous theorem that is easy to follow. There are many proofs already, but I thought I would try and see if I could give a slightly different one, and hope that it is clear. My thought is that sometimes the measure of clarity of a proof is the same as ``ownership'': if you wrote it---own it---then it is clear. But here goes a proof that is a bit different.

The overarching idea is to do two things: (i) avoid as much detailed encoding as possible, and (ii) leverage existing concepts that you probably already know.

Machines

Let $latex {L}&fg=000000$ be any set in $latex {\mathsf{NP}}&fg=000000$. Then there is always a one-tape nondeterministic Turing Machine (NTM) $latex {M}&fg=000000$ that accepts exactly $latex {L}&fg=000000$ and runs in time $latex {n^{k}}&fg=000000$ for some fixed $latex {k}&fg=000000$. For any input $latex {x}&fg=000000$ this means that $latex {M}&fg=000000$ accepts $latex {x}&fg=000000$ if and only if $latex {x}&fg=000000$ is in $latex {L}&fg=000000$. An ID $latex {U}&fg=000000$ of $latex {M}&fg=000000$ is an encoding of the total state of $latex {M}&fg=000000$ in the usual way. We have two special ID's:

For ID's,

$latex \displaystyle U \vdash V&fg=000000$

means that $latex {U}&fg=000000$ can reach $latex {V}&fg=000000$ in one step of $latex {M}&fg=000000$. This is all standard and is stated here just for review.

Saying that $latex {A}&fg=000000$ is an FSA means that $latex {A}&fg=000000$ is a deterministic finite state automaton. The language that $latex {A}&fg=000000$ accepts is $latex {L(A)}&fg=000000$. Also for any two strings $latex {x=x_{1},\dots,x_{n}}&fg=000000$ and $latex {y=y_{1},\dots,y_{n}}&fg=000000$ of the same length let $latex {x || y}&fg=000000$ be the shuffle,

$latex \displaystyle x_{1}\ y_{1}, \dots, x_{n} \ y_{n}. &fg=000000$

You might ask why introduce FSA when our goal is to encode NTM's? It turns out that our proof will take the following steps:
  1. Show that the behavior of an FSA can be encoded by $latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$, which is a more powerful version of $latex {\mathsf{SAT}}&fg=000000$. This version is easier to use and understand.
  2. Show that the behavior of a NTM can be reduced to the behavior of FSA's, and so to $latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$.
  3. Finally, replace $latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ by regular $latex {\mathsf{SAT}}&fg=000000$.

$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$

A $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ problem $latex {C}&fg=000000$ is of the following form:

$latex \displaystyle C = \exists x_{1} \exists x_{2} \cdots \exists x_{m} C_{1} \wedge \cdots \wedge C_{L}. &fg=000000$

Here each $latex {C_{i}}&fg=000000$ is a general clause, which means it is a Boolean function of the variables $latex {x_{i}}&fg=000000$'s. We allow the general-clauses to any Boolean function, but will restrict the number of variables that they can depend to at most $latex {k}&fg=000000$. The problem $latex {C}&fg=000000$ is called satisfiable provided there exists Boolean values for the variables $latex {x_{1},\dots,x_{m}}&fg=000000$ so that each $latex {C_{i}}&fg=000000$ evaluates to true.

Note that $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ is closed under conjunction in the following sense: Suppose that $latex {A}&fg=000000$ is

$latex \displaystyle A = \exists x_{1} \exists x_{2} \cdots \exists x_{m} A_{1} \wedge \cdots \wedge A_{K} &fg=000000$

and $latex {B}&fg=000000$ is

$latex \displaystyle B = \exists x_{1} \exists x_{2} \cdots \exists x_{m} B_{1} \wedge \cdots \wedge B_{L}. &fg=000000$

Then

$latex \displaystyle C = \exists x_{1} \exists x_{2} \cdots \exists x_{m} A_{1} \wedge \cdots \wedge A_{K} \wedge B_{1} \cdots \wedge B_{L}&fg=000000$

is the conjunction. This is satisfiable if and only if there are variables $latex {x_{i}}&fg=000000$ so that both sets of clauses are true. This is a simple, but very useful property of $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$.

There is nothing mysterious or strange about $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$. It is just a way of defining a type of search problem. Informally it asks: are there Boolean values $latex {\dots}&fg=000000$ that satisfy all of the properties $latex {\dots}&fg=000000$. We have lots of problems like this in mathematics. Consider a system of linear equations over the reals:

$latex \displaystyle Ax = b, &fg=000000$

where $latex {A}&fg=000000$ is a matrix, $latex {x}&fg=000000$ is a vector, and $latex {b}&fg=000000$ is a vector. The LINEAR problem is: does there exist a vector $latex {x}&fg=000000$ so that the above is true. We could have written it as

$latex \displaystyle \exists x Ax = b, &fg=000000$

to make it look like the $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ problem. You should, and probably do know, what Gauss knew years ago that LINEAR is ``easy'': in modern terms LINEAR is in $latex {\mathsf{P}}&fg=000000$, that is in polynomial time.

The difference between $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ and LINEAR is that while the latter is extremely useful and can be used to model many important problems, $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ is ``universal''. By universal we mean that any problem from $latex {\mathsf{NP}}&fg=000000$ can be reduced to solving a $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ problem.

Cook's Theorem

Our plan is to show that we can encode $latex {U \vdash V}&fg=000000$ by a $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ formula. Then the behavior of $latex {M}&fg=000000$ for $latex {n^{c}}&fg=000000$ steps will be encoded by simply using the fact that $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ is closed under conjunction.

Theorem 1 The problem $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ is $latex {\mathsf{NP}}&fg=000000$-complete.

Proof: Let $latex {M}&fg=000000$ be a one-tape NTM that runs in $latex {N=n^{c}}&fg=000000$ time and let $latex {x}&fg=000000$ be an input of length $latex {n}&fg=000000$. Clearly $latex {M}&fg=000000$ accepts if and only if there are exists a series of ID's

$latex \displaystyle S^{1},S^{2},\dots,S^{N} &fg=000000$

of length $latex {N}&fg=000000$ so that $latex {S^{1}}&fg=000000$ is the initial state, $latex {S^{N}}&fg=000000$ is a final accept state, and for each $latex {i}&fg=000000$,

$latex \displaystyle S^{i} \vdash S^{i+1}. &fg=000000$

Let $latex {S^{i}}&fg=000000$ for all $latex {i}&fg=000000$ consist of $latex {N}&fg=000000$ Boolean variables.

Claim: We have $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ formulas $latex {U^{i}}&fg=000000$ over these variables so that (i) $latex {U^{0}}&fg=000000$ is satisfied precisely when $latex {S^{1}}&fg=000000$ is the initial state corresponding to the input $latex {x}&fg=000000$; (ii) $latex {U^{N}}&fg=000000$ is satisfied precisely when $latex {S^{N}}&fg=000000$ corresponds to the final state; (iii) and for each $latex {1 \leq i < N}&fg=000000$, the $latex {U^{i}}&fg=000000$ is satisfied precisely if

$latex \displaystyle S^{i} \vdash S^{i+1}. &fg=000000$

Then we claim that the conjunction of the clauses of all the

$latex \displaystyle U^{1},\dots,U^{N}&fg=000000$

are satisfiable if and only if $latex {M}&fg=000000$ accepts. This follows directly by the definitions. $latex \Box&fg=000000$

Thus to complete the proof of the theorem we must show that claim about the existence of $latex {U^{i}}&fg=000000$'s is true. But this is easy as we will now show.

Encoding With FSA

Theorem 2 Let $latex {M}&fg=000000$ be a one-tape NTM. Then there is an FSA $latex {A}&fg=000000$ that depends only on $latex {M}&fg=000000$ so that for all $latex {U}&fg=000000$ and $latex {V}&fg=000000$,

$latex \displaystyle U \vdash V \text{ iff } U||V \in L(A). &fg=000000$

Proof: The FSA $latex {A}&fg=000000$ just passes over $latex {U}&fg=000000$ and $latex {V}&fg=000000$ checking that the tapes are the same, except at the location of the head. There it checks that a legal move of $latex {M}&fg=000000$ has been used. Because the ID's are shuffled together this can be done by the automaton. $latex \Box&fg=000000$

Encoding With $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$

Theorem 3 Let $latex {A}&fg=000000$ be a fixed FSA. Then for any input string $latex {a_{1},\dots,a_{n}}&fg=000000$ there are a set of general-clauses $latex {C}&fg=000000$ over $latex {O(n)}&fg=000000$ variables so that

$latex \displaystyle a_{1},\dots,a_{n} \in L(A) \text{ iff } C \text{ is satisfiable}. &fg=000000$

Proof: The idea is to look at the sequence

$latex \displaystyle q_{0} a_{1} q_{1} a_{1} \dots q_{n-1} a_{n} q_{n}, &fg=000000$

where $latex {q_{i}}&fg=000000$ are strings of Boolean variables that are long enough to encode the state of the FSA. Then the general-clauses are of three types:
  1. One clause that checks that $latex {q_{0}}&fg=000000$ is the start state of $latex {A}&fg=000000$.
  2. One clause that checks that $latex {q_{i+1}}&fg=000000$ is a possible state that $latex {q_{i}}&fg=000000$ can reach after seeing the input bit $latex {a_{i}}&fg=000000$.
  3. One clause that checks that $latex {q_{n}}&fg=000000$ is an accept state of $latex {A}&fg=000000$.
Clearly all of these can be done by general-clauses: they are just Boolean tests. $latex \Box&fg=000000$

$latex {\mathsf{SAT}}&fg=000000$

A $latex {\mathsf{3SAT}}&fg=000000$ problem $latex {C}&fg=000000$ is a $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ problem except that the clauses are restricted to be disjunctions of at most three variables and their negations. Thus a clause can only be of the form

$latex \displaystyle (x_{20} \vee x_{30} \vee \bar{x}_{101}), &fg=000000$

for example.

The final step is to note:

Theorem 4 The problem $latex {k}&fg=000000$-$latex {\mathsf{GEN}}&fg=000000$-$latex {\mathsf{SAT}}&fg=000000$ can be reduced to $latex {\mathsf{SAT}}&fg=000000$.

This proves Cook's Theorem.

Nand Now For Something Different

Ken tells me that especially in Buffalo's undergraduate theory course, he uses---and gets away with---a big handwave. He states the principle

``Software Can Be Efficiently Burned Into Hardware''

to assert that the witness predicate $latex {R(x,y)}&fg=000000$ for a given $latex {\mathsf{NP}}&fg=000000$-language $latex {L}&fg=000000$ can be replaced by a polynomial-sized circuit $latex {C_n}&fg=000000$ for any input length $latex {n}&fg=000000$. Since NAND gates are universal, every gate can be a binary NAND. Thus $latex {x \in L}&fg=000000$ if and only if there exist a $latex {y}&fg=000000$ and an assignment to every wire in $latex {C_n}&fg=000000$ that is consistent with every NAND gate, such that the output wire $latex {w_o}&fg=000000$ has value $latex {1}&fg=000000$. For the inputs $latex {u,v}&fg=000000$ and every output $latex {w}&fg=000000$ of each NAND gate, the assignment must satisfy the clauses

$latex \displaystyle (u \vee w) \wedge (v \vee w) \wedge (\bar{u} \vee \bar{v} \vee \bar{w}).&fg=000000$

Together with the singleton clause $latex {(w_0)}&fg=000000$ and clauses fixing the wires for $latex {x_i}&fg=000000$ to the corresponding bits of the given input string $latex {x}&fg=000000$, this creates a $latex {\mathsf{3SAT}}&fg=000000$ formula that is satisfiable if and only if $latex {x \in L}&fg=000000$.

This proof has some nice features---it shows the completeness of several restricted forms of $latex {\mathsf{3SAT}}&fg=000000$ where the variables in each clause have the same sign and (with a little more work) assignments must make at least one literal in each clause false as well. But it hides the way computations are represented behind the handwave.

Open Problems

What do you think of the proof via finite automata?