The Ryan Williams Combine
Structuring his famous proof to build more on it
Ryan Williams is a deep theorist who is known among other things for his frontier-setting lower bounds against circuits. There is also a professional football player named Ryan Williams who played for Virginia Tech in the ACC college conference. The football Ryan had a sub-par showing at the 2011 NFL Combine, which is a series of exercises use by pro scouts to evaluate players, but still became an early second-round pick in the 2011 NFL Draft. Unfortunately he was injured for the entire 2011 NFL season and is out for the rest of this season too. Happily injuries are less of a concern for our Ryan Williams, who married a Virginia.
Today we make a “combine” out of Ryan’s famous lower bound proof. That is, we present it as a series of separate tasks that let us scout opportunities to improve the theorems.
Of course the proof is completely his—this is nothing more than a rearrangement to emphasize different ways that computational problems related to succinctness are employed. We tried to explain the proof two years ago right after it came out, but were not completely successful. Here we will try again with this particular theorem in the paper:
Theorem 1. The complexity class is not contained in .
Ryan proves further lower bounds in his paper, but focusing on this one enables us to skirt some technical issues and make the presentation mostly self-contained. We will try to see what properties of are exploited, and what hypotheses are needed, in order to make this apply to a general circuit class .
Our framework builds on the notion of circuits that describe a Boolean string. For a circuit with inputs , let be the result of evaluating on the input . Also we identify strings of length with the integers
Definition 2. Say that circuit describes the Boolean string provided
We will use to denote this.
The similar capital letter is deliberate. can be an encoding of another circuit , or a computation by a circuit, or an assignment to a Boolean formula on variables.
We encode general Boolean circuits as directed acyclic graphs using gate types AND, OR, NOT, and INPUT of fan-in at most two. The size of such a circuit is the number of gates. An circuit allows unbounded fan-in gates AND, OR, and MOD for some fixed as usual. Its size is the number of wires, and its depth is a constant independent of the number of input gates.
We allow sizes that are greater than polynomial—indeed we write to mean a quasi-polynomial function, namely one bounded by for some polynomial . Note that a circuit of size needs only bits to encode. Extra log factors will affect some (sub-)exponential running times, but will not matter to the circuit size bounds. We write to denote circuits of size . Ryan’s paper proves bounds against circuits of size where is a higher function; we keep ‘s quasi-polynomial to save on details, but hope the general notation helps readers who wish to proceed to the stronger results.
Circuit Problems and the Key Property
For a moment think of as any kind of circuit or Turing machine, or even a non-deterministic random-access machine. Given and a length , consider these four problems:
- Evaluate: Given an input of length , what is ?
- Evaluate-all: Evaluate on all inputs of length .
- Satisfiability: Is there an of length such that ?
- Equivalence: Given circuits , is there (not) an input of length such that ?
If is a circuit of encoding size , or a machine running in time , then the notional times to solve these problems deterministically are for the first, and for the others. If (and ) are a non-deterministic machine(s) running in time , then there exists a small witness for satisfiability, but not necessarily for inequivalence. An important detail is that even if is a non-deterministic RAM running in time , there is a non-deterministic TM that simulates it with only overhead (by “reduction to sorting”). This implies we can get a witness of size , and also allows us to apply an efficient Cook-Levin construction that works for NTM’s.
The key property of the circuit class is that it can beat the notional time for evaluate-all, in a way that enables even better times for the last two problems. We have talked in general before about new lower bounds flowing from new upper bounds. The general framework is:
- Prove a better-than-notional upper bound for the target class on one of the problems.
- Make a hypothesis that would amplify the power of .
- Show this implies a better-than-notional speedup that is actually impossible.
- Conclude as a theorem, from which lower bounds follow.
Ryan’s proof translates a tiny savings for satisfiability of circuits into a bigger savings for exponential-time NTMs, one that violates the nondeterministic time hierarchy theorem.
The ACC Algorithms
First we state what is called the “fast evaluation lemma”:
Lemma 3. For any quasi-polynomial , we can build an algorithm that evaluates a given -input -circuit on all inputs in time .
There are three proofs of this now: a matrix based one, a dynamic programming one, and a newer one based on a simple divide and conquer method. For now just take this as true. Now we see how this can be amplified to create a better time for satisfiability and equivalence. We call the following the fast algorithm for circuits.
Proof. Select of the inputs of the circuit . Form all the circuits by setting the inputs to all possible values. Then form the new circuit that is the OR of all these circuits. Clearly is satisfiable if and only if is. Further is a circuit. Now evaluate on all the inputs. By the fast evaluation lemma this takes time
It suffices to make a large enough multiple of to achieve time .
Note that there is some slack: we could take to be a polynomial in , and would still have quasi-polynomial size. We are abusing notation in whether means quasi-polynomial in general or a particulat size, but the usage should be clear in context.
The additional closure properties needed of a circuit class , besides the key speedup, are closure under exclusive-or as used here, closure under composition as used later, and a mix of composition and Boolean operations needed for the “replacement lemma” below. It is not clear whether we need to make the depth of the composed circuits explicit in the framework. The particular depth values matter most to quantifying optimal bounds in Ryan’s proof. If the depth needs to be stated up front, at least it applies when trying to prove lower bounds against in place of .
The key hypothesis we state for sake of contradiction is:
Hypothesis H. The complexity class has circuits.
Note this also implies has circuits, which we call hypothesis H*.
Hypothesis H is stronger than the actual assumption used in Ryan’s paper. The point here is that this simpler assumption will make some of the details less technical, while the ideas and strategy are exactly the same as in the full version. The paper also proves lower bounds against , which is not known to contain . For this an “easy-witness” property that follows from is used, but this time we will avoid it.
Having explained why is the target for the lower bound, why do we have at the upper end? Part of this comes from the following meta-comment about the general approach: In many parts of the proof circuits of type have to be constructed by an algorithm. In many cases there is no way to deterministically construct the circuits—at least none that are known. The approach used is based on a three-step method:
- Show via the above assumption that the required circuit must exist. This only requires that the computation that the circuit performs can be done in the class .
- Guess the required circuit .
- Then verify that the guessed circuit is correct. This is exactly where the speedups on equivalence and satisfiability are used.
The special reason for is that the construction builds exponentially large strings that are used as oracle queries to an oracle. The hypotheses and allow us to replace all this by circuits.
Given a language , let stand for the -length bit string of membership results on . The proof needs only the weaker hypothesis H*, twice.
Proof. By , the algorithm can generate a uniform sequence of polynomial-size circuits such that . The goal is to guess and verify , so that . However, we cannot directly appeal to equivalence testing being in time because is not a circuit but a general circuit.
The trick is to guess a that verifies the computation of doing evaluate-all on . This is represented by the language
where we think of . Then is also in , so applying hypothesis here implies the ability to guess a -circuit with inputs (for some fixed ) such that . The point is that we can verify the correctness of locally at all gates, including the final output gate .
To do this verification, we need to represent the encoding of . We could do this as a single layer of gates computing functions where has a and where has a . However, to illustrate what we can build in , we instead use again to guess a -circuit with inputs such that . In this case can in fact have polynomial size, and verifying can be done by brute force evaluation on all possible inputs.
The final circuit stitches together and and ultimately outputs . This evaluate-all task operates within time since is a -circuit. It remains to argue that the verification of the guessed circuit , in-tandem with the already-verified circuit , can be reduced to – and hence completed in time. For this we have build out of and yet one more circuit with inputs that works as follows:
On input , if are not the inputs to according to then reject. If so, make calls and to get their values, and compare with the value . If the values are not correct for the gate , then accept, else reject.
Then is correct if and only if is unsatisfiable. Given an exponent from Theorem 4, this takes time
Taking great enough, as we are able to do, makes the denominator exceed . Note that is a Boolean combination of three calls to and three references to , so it is a circuit.
The remaining tasks translate an NTM running in time into a succinct formula on variables, using a known efficient form of the Cook-Levin construction. The following “checking lemma” helps us verify assignments to such formulas.
Lemma 6. Suppose that and , where and are circuits with inputs. Then for any , there is a deterministic algorithm that runs in time and checks whether is a valid assignment to the 3-CNF formula encoded by .
Proof. We will construct a new circuit with inputs. Essentially the circuit “looks for” a clause that is unsatisfied. The circuit on input computes the clause encoded by . It does this by accessing consecutive bits of the string , using on consecutive locations to do this. If these bits do not encode a clause, the algorithm rejects. If they do encode a clause, it then finds the three variables used in the clause and whether they are negated. Then it looks up the values of by using three times. Finally if the clause is not satisfied it returns accept; otherwise, it returns reject. It is clear this can be done as a circuit with inputs.
The algorithm then must determine whether or not ever accepts. Note accepts only if “points” to a proper clause in that is not satisfied. Similar to the end of the replacement lemma’s proof, it does this by appeal to the fast – algorithm.
We note that the checking lemma could be extended to check other “local” properties, but this is enough for the main proof.
Strong Cook-Levin Construction
The following is a known theorem that exploits the locality of the Cook-Levin construction.
Theorem 7. There is a constant such that for any language in there is a deterministic polynomial time algorithm that given input of length outputs a circuit with at most inputs and size such that , where is a 3-CNF formula of size at most such that is in if and only if is satisfiable.
With , the proof takes a time- witness predicate for , converts it into circuits of size that decide , and writes a 3-CNF formula in variables whose clauses verify that each gate of has correct output for its inputs.
Corollary 8. Using the notation of the above theorem, whenever is a string of length belonging to , there exists a circuit with at most inputs such that , where is the lexicographically first satisfying assignment to .
Proof. Construct the formula which is of size at most . Use the oracle to find a satisfying assignment, and use it further to do a binary search that finds the lexicographically first one. Since this is done by an algorithm, Hypothesis implies the existence of equivalent circuits in .
To explain a potentially confusing point, note that the proof requires making calls to the oracle on exponentially large strings, since the formula is exponentially large. This is allowed in .
Assembling The Proof
Now we combine all these parts into the final theorem and proof.
Proof. Recall we begin by assuming that is contained in , which entails that is also in
Now suppose we have a language that is accepted by an NTM running in time . We will show that it can be accepted by a NTM that runs in time for some . This contradiction of the nondeterministic time hierarchy theorem completes the proof.
We break the proof into steps. Let be an input.
(1): Construct a polynomial-size general circuit so that where is a 3-CNF formula that is satisfiable if and only if is in . Note is of size and thus has inputs for some . Note the existence and the ability to create the circuit in polynomial time are based on the Strong Cook-Levin Theorem 7.
(2): Use our replacement lemma 5 to find a circuit so that . This circuit has quasi-polynomial size and inputs—not necessarily the same as for the circuit in the proof of that lemma.
(3): Now guess another circuit with inputs and quasi-polynomial size so that where is satisfying assignment to . This uses Corollary 8.
(4): Finally accept if is actually such an assignment. This uses the checking lemma 6.
All of this can be done in the required time, and we have a contradiction.
Can we apply the framework to prove lower bounds against other classes ? Does this help us seek for such ? Can we do it with or even ? Can assuming help with the latter?