Ryan Williams
email: ryanwill@us.ibm.com

ALTERNATION-TRADING PROOFS, LINEAR PROGRAMMING, AND LOWER BOUNDS (EXTENDED ABSTRACT)

Keywords: Subject Classification: F.2.3, I.2.3 time-space tradeoffs, lower bounds, alternation, linear programming

A fertile area of recent research has demonstrated concrete polynomial time lower bounds for solving natural hard problems on restricted computational models. Among these problems are Satisfiability, Vertex Cover, Hamilton Path, MOD6-SAT, Majority-of-Majority-SAT, and Tautologies, to name a few. The proofs of these lower bounds follow a certain proof-by-contradiction strategy that we call alternation-trading. An important open problem is to determine how powerful such proofs can possibly be.

We propose a methodology for studying these proofs that makes them amenable to both formal analysis and automated theorem proving. We prove that the search for better lower bounds can often be turned into a problem of solving a large series of linear programming instances. Implementing a small-scale theorem prover based on this result, we extract new human-readable time lower bounds for several problems. This framework can also be used to prove concrete limitations on the current techniques.

Introduction

Many known lower bounds for natural problems follow a type of algorithmic argument that we call a resource-trading proof. Such a proof assumes that a hard problem can be solved by a "good" algorithm, and tries to derive a contradiction by combining two essential components. One is a speedup lemma, which simulates all good algorithms super-efficiently on some "interesting" computational model, trading time for some resource. The second component is a slowdown lemma, which uses the assumed good algorithm for the hard problem to simulate computations from the "interesting" model by good algorithms, thereby trading the "interesting" resource for more time. Clever combinations of speedup and slowdown lemmas are used to contradict a known result, in particular some complexity hierarchy theorem. That is, by assuming a "good" algorithm for a hard problem, we derive something like TIME[n 2 ] ⊆ TIME[n], a contradiction.

As an example, one can prove a time-space tradeoff for satisfiability (SAT) as follows. Assume SAT has an algorithm running in n c time and poly(log n) space, for some c > 1. One speedup lemma is that computations running in n a time and poly(log n) space can be simulated by an alternating machine that switches from co-nondeterministic mode to nondeterministic mode once (i.e., a Π 2 machine), and runs in n a/2+o(1) time. This speedup lemma trades time for alternations. The relevant slowdown lemma is: if SAT has an n c time, poly(log n) space algorithm, then (by a strengthening of the Cook-Levin theorem) every language in NTIME[t] has t c+o(1) time, poly(log t) space algorithms. Consequently, an alternating machine running in t time and making k -1 alternations has t c k +o(1) time, poly(log t) space algorithms. Combining these speedup and slowdown lemmas, we derive

Σ 2 TIME[t] ⊆ DTISP[t c 2 +o(1) , poly(log t)] ⊆ Π 2 TIME[t c 2 /2 ],
where the first inclusion holds by slowdown and the second holds by speedup. Now observe that the alternating time hierarchy is contradicted when c 2 < 2. This proof is the n

√ 2-ε
time lower bound of Lipton and Viglas [START_REF] Lipton | On the complexity of SAT[END_REF]. Some of the best known separations in complexity theory use resource-trading proofs. Hopcroft, Paul, and Valiant [START_REF] Hopcroft | On time versus space[END_REF] showed that SPACE[n] DTIME[o(n log n)] for multitape Turing machines, by proving the "speedup lemma" that DTIME[t] ⊆ SPACE[t/ log t] and invoking diagonalization. Their result was later extended to general models [START_REF] Paul | On time versus space II[END_REF][START_REF] Halpern | On Time versus Space III[END_REF]. Paul, Pippenger, Szemeredi, and Trotter [START_REF] Paul | On determinism versus nondeterminism and related problems[END_REF] proved that NTIME[n] = DTIME [n] for multitape Turing machines. The key component in the proof is the "speedup lemma" DTIME[t] ⊆ Σ 4 TIME[t/ log * t] for multitape TMs. Despite their age, the above separations still constitute the best known progress on P vs PSPACE and P vs NP, respectively.

In more recent years, resource-trading proofs have established time-space lower bounds for NP-complete problems and problems higher in the polynomial hierarchy [Kan84, For97, LV99, FvM00, FLvMV05, Wil06, Wil08]. For instance, the best known time lower bound for solving SAT with n o(1) -space algorithms is n 2 cos(π/7)-o(1) ≥ n 1.801 , obtained with a resourcetrading proof [START_REF] Williams | Time-space tradeoffs for counting NP solutions modulo integers[END_REF]. (Note if one could improve the 1.801 exponent to arbitrary constants, one would separate LOGSPACE from NP.) For nondeterministic algorithms using n o(1) space, the best known time lower bound for solving the coNP-complete Tautology problem was n √ 2-o(1) for several years [START_REF] Fortnow | Time-Space Tradeoffs for Nondeterministic Computation[END_REF]. Certain time-space lower bounds for probabilistic and quantum computations also follow the resource-trading paradigm [START_REF] Allender | Time-space tradeoffs in the counting hierarchy[END_REF][START_REF] Diehl | Time-space lower bounds for the polynomial-time hierarchy on randomized machines[END_REF][START_REF] Viola | On approximate majority and probabilistic time[END_REF][START_REF] Van Melkebeek | A quantum time-space lower bound for the counting hierarchy[END_REF]. Resource-trading proofs are also abound in the multidimensional "hybrid" Turing machine model, which has read-only random access to its input and an n o(1) readwrite store, as well as read-write two-way access to a d-dimensional tape for some d ≥ 1. This is the most powerful (and physically realistic) model known where we still know nontrivial time lower bounds for problems such as SAT. Multidimensional TMs have a long history; e.g., [START_REF] Loui | Simulations among multidimensional Turing machines[END_REF][START_REF] Paul | On time versus space II[END_REF][START_REF] Kannan | Alternation and the power of nondeterminism[END_REF][START_REF] Maass | Speed-up of Turing machines with one work tape and a two-way input tape[END_REF][START_REF] Van Melkebeek | A time lower bound for satisfiability[END_REF][START_REF] Williams | Inductive time-space lower bounds for SAT and related problems[END_REF] proved lower bounds for them. (For a more complete literature review, please see the full version of the paper.)

Main Results

We introduce a methodology for reasoning about resource-trading proofs that is also practically implementable for finding short proofs. Informally, the "hard work" in these proofs can be replaced by solving a series of linear programming problems. This perspective not only aids us practically in the search for new lower bounds, but also allows us to show non-trivial limitations on what can be proved.

This methodology is applied to several lower bound problems. In all cases considered here, the resource being "traded" is alternations, so we call the proofs alternation-trading. Deterministic Time-Space Lower Bounds. Aided by results of a computer program, we show that any SAT algorithm running in t(n) time and s(n) space satisfies t•s ≥ Ω(n 2 cos(π/7)-o(1) ). Previously, the best known result was t • s ≥ Ω(n 1.573 ) [START_REF] Fortnow | Time-Space Lower Bounds for Satisfiability[END_REF]. It has been conjectured that the current framework sufficed to prove a n 2-o(1) time lower bound for SAT, against algorithms using n o(1) space. We prove that it is not possible to obtain n 2 with the framework, formalizing a conjecture of [START_REF] Fortnow | Time-Space Lower Bounds for Satisfiability[END_REF]. * A computer search over proofs of short length suggests that the best known n 2 cos(π/7)-o(1) lower bound [START_REF] Williams | Time-space tradeoffs for counting NP solutions modulo integers[END_REF] is already optimal for the framework. We also prove lower bounds on QBF k (quantified Boolean formulas with at most k quantifier blocks), showing that the problem requires Ω(n k+1-δ k ) time for n o(1) space algorithms, where δ k < 0.2 and lim k→∞ δ k = 0. † Nondeterministic Time-Space Lower Bounds. Adapting our ideas to proving lower bounds for Tautologies, a computer program found a very short proof improving upon Fortnow and Van Melkebeek's lower bound. Longer proofs suggested an interesting pattern. Joint work with Diehl and Van Melkebeek on this observation resulted in an n 4 1/3 -o(1) ≥ n 1.587 time lower bound [START_REF] Diehl | An improved time-space lower bound for tautologies[END_REF]. Computer search suggests that this lower bound is best possible for the framework. We prove that it is not possible to obtain an n φ time lower bound, where φ = 1.618 . . . is the golden ratio. This is surprising since we have known for some time that an n φ lower bound is provable for deterministic algorithms [START_REF] Fortnow | Time-Space Tradeoffs for Nondeterministic Computation[END_REF]. Multidimensional Turing Machine Lower Bounds. Here our method uncovers peculiar behavior in the best lower bound proofs, regardless of the dimension. Studying computer search results, we extract an Ω(n r d ) time lower bound for the d-dimensional case, where r d ≥ 1 is the root of a particular quintic p d (x) with coefficients depending on d. For example, r 1 ≈ 1.3009, r 2 ≈ 1.1887, and r 3 ≈ 1.1372. Again, our search suggests this is best possible, and we can prove it is not possible to improve the bound for d-dimensional TMs to n 1+1/(d+1) with the current tools.

These limitations also hold for other NP and coNP-hard problems; the only property required is that all languages in NTIME[n] (respectively, coNTIME[n]) have sufficiently efficient reductions to the problem. Also our linear programming approach is not limited to the above, and can be applied to the league of lower bounds discussed in Van Melkebeek's surveys [vM04, vM07].

Some Remarks on the Reduction to Linear Programming

The key to our formulation is to separate the discrete choices in an alternation-trading proof from the real-valued choices. The discrete choices consist of the sequence of lemmas to apply in each step, and what sort of hierarchy theorem to use in the contradiction. We present several simplifications that greatly reduce the number of discrete choices, without loss of generality. The real-valued choices are the running time exponents that arise from * That is, we formalize the statement: "...some complexity theorists feel that improving the golden ratio exponent beyond 2 would require a breakthrough" in Section 8 of [START_REF] Fortnow | Time-Space Lower Bounds for Satisfiability[END_REF]. † Note the QBF k results appeared in the author's PhD thesis in 2007 but have been unpublished to date.

the choices of time bounds and rule applications. We prove that once the discrete choices are made, the remaining real-valued problem can be expressed as an instance of linear programming. This makes it possible to search for new proofs via computer, and it also gives us a formal handle on the limitations of these proofs.

One cannot easily search over all possible proofs, as the number of discrete choices is still about 2 n /n 3/2 for proofs of n lines (proportional to the nth Catalan number). Nevertheless it is still feasible to try all 24+ line proofs. These proof searches reveal patterns, indicating that certain strategies will be most successful in proving lower bounds; in each case we study, the resulting strategies differ. Following the strategies, we establish new lower bound proofs. The patterns also suggest how to show limitations on the proof systems. Note: Due to space limitations, we can only describe how our methods apply to SAT timespace lower bounds. Please see the full version of the paper for proofs and more details.

Preliminaries

We assume familiarity with Complexity Theory, especially the notion of alternationWe use big-Ω notation in the infinitely often sense, so statements like "SAT is not in O(n c ) time" are equivalent to "SAT requires Ω(n c ) time." All functions are assumed constructible within the appropriate bounds. Our default computational model is the random access machine, broadly construed: particular variants do not affect the results. DTISP[t(n), s(n)] is the class of languages accepted by a RAM running in t(n) time and s(n) space, simultaneously. For convenience, we set

DTS[t(n)] := DTISP[t(n) 1+o(1) , n o(1) ] to omit negligible o(1) factors.
In order to properly formalize alternation-trading proofs, we introduce notation for alternating complexity classes that include input constraints between alternations. Let us start with an example of the notation, then give a general definition. Define (∃ f (n)) b DTS[n a ] to be the class of languages recognized by a machine which, on an input x of length n, writes a f (n) 1+o(1) bit string y nondeterministically, copies at most n b+o(1) bits z from the pair x, y (in O(n b+o(1) ) time), then feeds z as input to a machine M running in n a+o(1) time and n o(1) space. Note the runtime of M is measured with respect to the initial input length n, not the latter input length n b+o(1) of z.

We generalize this definition as follows. Let C be a complexity class. For i = 1, . . . , k, let

Q i ∈ {∃, ∀} and a i , b i ≥ 0. Define (Q 1 n a 1 ) b 2 (Q 2 n a 2 ) • • • b k (Q k n a k ) b k+1 C
to be the class of languages recognized by a machine M that, on input x of length n, has the following general behavior on input x:

Set z 0 := x. For i = 1, . . . , k, If Q i = ∃, switch to existential mode. If Q i = ∀, switch to universal mode.
Guess an n a i +o(1) bit string y (universally or existentially).

Copy at most n b i+1 +o(1) bits z i from the pair z i-1 , y . End for Run a machine recognizing a language in class C on the input z k . When an input constraint b i is unspecified, its default value is max{a i , 1}. We say that the existential and universal modes of an alternating computation are quantifier blocks, to reflect the complexity class notation. It is crucial to observe that the time bound in the ith quantifier block is measured with respect to n, the input to the first quantifier block.

Notice that by simple properties of nondeterminism and conondeterminism, we can combine adjacent quantifier blocks that are of the same type, e.g., (∃n a ) a (∃n b ) b DTS[n c ] = (∃n max{a,b} ) b DTS[n c ]. This useful property is exploited in alternation-trading proofs.

A Short Introduction to Alternation-Trading Proofs

Here we give a brief overview of the tools used in alternation-trading proofs. In this extended abstract we focus on deterministic time lower bounds for satisfiability for algorithms using n o(1) workspace; the other lower bound problems use similar tools.

It is known that satisfiability of Boolean formulas in conjunctive normal form (SAT) is a complete problem under tight reductions for a small nondeterministic complexity class. The class NQL, called nondeterministic quasilinear time, is defined as [START_REF] Schnorr | Satisfiability is quasilinear complete in NQL[END_REF][START_REF] Tourlakis | Time-space tradeoffs for SAT on nonuniform machines[END_REF][START_REF] Fortnow | Time-Space Lower Bounds for Satisfiability[END_REF]). SAT is NQL-complete under quasilinear time O(log n) space reductions, for both multitape and random access machine models. Moreover, each bit of the reduction can be computed in O(poly(log n)) time and O(log n) space in both machine models. ‡ Let C[t(n)] represent a time t(n) complexity class under one of the three models:

NQL := c≥0 NTIME[n • (log n) c ] = NTIME[n • poly(log n)]. Theorem 2.1 ([Coo88,
• deterministic RAM using time t and t o(1) space, • co-nondeterministic RAM using time t and t o(1) space, • d-dimensional Turing machine using time t.

Theorem 2.1 implies that if NTIME[n] C[t], then SAT / ∈ C[t/poly(log t)]. Corollary 2.2. If NTIME[n] C[t(n)], then SAT / ∈ C[t(n)/ log k t(n)] for some k > 0.
Hence we wish to prove NTIME[n] C[n c ] for large c > 1. To prove time-space lower bounds, we work with

C[n c ] = DTS[n c ] = DTISP[n c , n o(1)
]. Van Melkebeek and Raz [START_REF] Van Melkebeek | A time lower bound for satisfiability[END_REF] observed that a similar corollary holds for any problem Π such that SAT reduces to Π under highly efficient reductions, e.g. Vertex Cover, Hamilton Path, 3-SAT, and Max-2-Sat. Therefore similar time lower bounds hold for these problems as well.

Speedups, Slowdowns, and Contradictions. Now that our goal is to prove NTIME[n] DTS[n c ], how can we do this? In an alternation-trading proof, we attempt to establish a contradiction from assuming NTIME[n] ⊆ DTS[n c ], by applying two lemmas which complement one another. A speedup lemma takes a DTS[t] class and places it in an alternating class with runtime o(t). A slowdown lemma takes an alternating class with runtime t and places it in a class with one less alternation and runtime O(t c ). The Speedup Lemma dates back to Nepomnjascii [START_REF] Nepomnjascii | Rudimentary predicates and Turing calculations[END_REF] and Kannan [START_REF] Kannan | Towards separating nondeterminism from determinism[END_REF]. ‡

In the multitape Turing machine model we assume that the tape heads are already oriented on the appropriate cells, otherwise it may take linear time to find the appropriate cells on a tape.

Lemma 2.3 (Speedup Lemma). Let a ≥ 1, e ≥ 0 and 0 ≤ x ≤ a. Then

DTISP[n a , n e ] ⊆ (Q 1 n x+e ) max{1,x+e} (Q 2 log n) max{1,e} DTISP[n a-x , n e ],
for

Q i ∈ {∃, ∀} where Q 1 = Q 2 . In particular, DTS[n a ] ⊆ (Q 1 n x ) max{1,x} (Q 2 log n) 1 DTS[n a-x ].
Proof. Let M use n a time and n e space. Let y be an input of length n. A complete description (i.e. configuration) of M (y) at any step can be described in O(n e + log n) space. To simulate M in (∃ n x+e ) max{1,x+e} (∀ log n) max{1,e} DTISP[n a-x , n e ], the algorithm N (y) existentially guesses a sequence of configurations C 1 , . . . , C n x of M (x). Then N (y) appends the initial configuration C 0 of M (y) to the beginning of the sequence, and an accepting configuration C n x +1 to the end. N (y) universally guesses a i ∈ {0, . . . , n x }, erases all configurations except C i and C i+1 , then simulates M (y) starting from C i , accepting if and only if C i+1 is reached within n a-x steps. It is easy to see the simulation is correct. The input constraints on the quantifier blocks are satisfied since after the universal guess, the input is only y, C i , and C i+1 , which is of size n + 2n e+o(1) ≤ n max{1,e}+o(1) . Observe in the above alternating simulation, the input to the final DTISP computation is linear in n + n e , regardless of the choice of x. This is a subtle property that is exploited heavily in alternation-trading proofs. The Slowdown Lemma is the following simple result:

Lemma 2.4 (Slowdown Lemma). Let a ≥ 1, e ≥ 0, a ′ ≥ 0, and b ≥ 1. If NTIME[n] ⊆ DTISP[n c , n e ], then for both Q ∈ {∃, ∀}, (Q n a ′ ) b DTIME[n a ] ⊆ DTISP[n c•max{a,a ′ ,b} , n e•max{a,a ′ ,b} ]. In particular, if NTIME[n] ⊆ DTS[n c ], then (Q n a ′ ) b DTIME[n a ] ⊆ DTS[n c•max{a,a ′ ,b} ].
Proof. Let L be a problem in (Q n a ′ ) b DTIME[n a ], and let A be an algorithm recognizing L. On an input x of length n, A guesses a string y of length n a ′ +o(1) and feeds an n b+o(1) bit string z to A ′ (z), where A ′ is a deterministic algorithm that runs in n a time. Since NTIME[n] ⊆ DTISP[n c , n e ] and DTISP is closed under complement, by padding we have

NTIME[p(n)] ∪ coNTIME[p(n)] ⊆ DTISP[p(n) c , p(n) e ]
for polynomials p(n) ≥ n. Therefore A can be simulated with a deterministic algorithm B. Since the runtime of A is n a ′ +o(1) + n b+o(1) + n a , the runtime of B is n c•max{a,a ′ ,b}+o(1) and the space usage is similar.

The final component of an alternation-trading proof is a time hierarchy theorem, the most general of which is the following, provable by a simple diagonalization.

Theorem 2.5 (Alternating Time Hierarchy). For k ≥ 0, for all

Q i ∈ {∃, ∀}, 1 ≤ a ′ i < a i , and 1 ≤ b ′ i ≤ b i , (Q 1 n a 1 ) b 2 • • • b k (Q k n a k ) b k+1 DTS[n a k+1 ] (R 1 n a ′ 1 ) b ′ 2 • • • b ′ k (R k n a ′ k ) b ′ k+1 DTS[n a ′ k+1 ],
where R i ∈ {∃, ∀} and R i = Q i for all i = 2, . . . , k + 1.

Two Examples. Let us give a couple of examples of alternation-trading proofs.

To simplify the presentation we do not specify the input constraints to quantifiers in the below.

(1) In FOCS'99, Lipton and Viglas proved that SAT cannot be solved by algorithms running in n √ 2-ε time and n o(1) space, for all ε > 0. By Theorem 2.1, if SAT is in n √ 2-ε time and n o(1) space then NTIME[n] ⊆ DTS[n c ] with c 2 < 2. We have Example (2) was discovered by a computer program. By "discovered", we mean that the program applied speedups and slowdowns in precisely the same way, having only minimum knowledge of the lemmas. Furthermore, the program verified that above is the best possible alternation-trading proof that applies the Speedup and Slowdown Lemmas at most 7 times. A more formal definition of "alternation-trading proof" is given in the next section.

(∃ n 2/c 2 )(∀ n 2/c 2 )DTS[n 2/c 2 ] ⊆ (∃ n 2/c 2 )DTS[n 2/c ] (Slowdown Lemma) ⊆ DTS[n 2 ] (Slowdown Lemma) ⊆ (∀ n)(∃ log n)DTS[n]. (Speedup Lemma, with x = 1) But (∃ n 2/c 2 )(∀ n 2/c 2 )DTS[n 2/c 2 ] ⊆ (∀ n)(∃ log n)DTS[n]
DTS[n c 2 /2+2 ] ⊆ (∃ n c 2 /2 )(∀ log n)DTS[n 2 ] (Speedup) ⊆ (∃ n c 2 /2 )(∀ log n)(∀ n)(∃ log n)DTS[n] (Speedup) = (∃ n c 2 /2 )(∀ n)(∃ log n)DTS[n] (Combining ∀ Quantifiers) ⊆ (∃ n c 2 /2 )(∀ n)DTS[n c ] (Slowdown) ⊆ (∃ n c 2 /2 )DTS[n c 2 ] (Slowdown) ⊆ (∃ n c 2 /2 )(∃ n c 2 /2 )(∀ log n)DTS[n c 2 /2 ] (Speedup) = (∃ n c 2 /2 )(∀ log n)DTS[n c 2 /2 ] (Combining ∃ Quantifiers) ⊆ (∃ n c 2 /2 )DTS[n c 3 /2 ] (Slowdown) ⊆ DTS[n c

Formalizing Alternation-Trading Proofs

We formalize alternation-trading proofs of lower bounds on DTS classes as follows: ¶ 3.1. Let c > 1. An alternation-trading proof for c is a list of complexity classes of the form: 1) ]. The first assumption, along with the Speedup and Slowdown Lemmas, implies that for every k there's a 1) ], which contradicts the time hierarchy for Σ2TIME. ¶ This formalization has implicitly appeared in several prior works, but not to the degree that we investigate in this paper.

(Q 1 n a 1 ) b 2 (Q 2 n a 2 ) • • • b k (Q k n a k ) b k+1 DTS[n a k+1 ], (3.1) § Suppose NTIME[n] ⊆ DTS[n c ] and Σ2TIME[n] ⊆ Π2TIME[n 1+o(
K satisfying Σ2TIME[n k ] ⊆ NTIME[n kc ] ⊆ ΣK TIME[n]. But the second assumption implies that ΣK TIME[n] = Σ2TIME[n 1+o(1) ]. Hence Σ2TIME[n k ] ⊆ Σ2TIME[n 1+o(
where k ≥ 0, Q i ∈ {∃, ∀}, Q i = Q i+1 , a i > 0, and b i ≥ 1, for all i. (When k = 0, the class is deterministic.) The items of the list are called lines of the proof. Each line is obtained from the previous line by applying either a speedup rule or a slowdown rule. More precisely, if the ith line is

(Q 1 n a 1 ) b 2 (Q 2 n a 2 ) • • • b k (Q k n a k ) b k+1 DTS[n a k+1 ]
, then the (i + 1)st line has one of four possible forms: Speedup Rule 0: For k = 0 and any x ∈ (0, a 1 ), (Q

0 n x ) max{x,1} (Q 1 n 0 ) 1 DTS[n a 1 -x ].
Speedup Rule 1: For k > 0 and any x ∈ (0, a k+1 ),

(Q 1 n a 1 ) b 2 (Q 2 n a 2 ) • • • b k (Q k n max{a k ,x} ) max{x,b k+1 } (Q k+1 n 0 ) b k+1 DTS[n a k+1 -x ].
Speedup Rule 2: For k > 0 and any x ∈ (0, a k+1 ),

(Q 1 n a 1 ) b 2 • • • b k (Q k n a k ) b k+1 (Q k+1 n x ) max{x,b k+1 } (Q k+2 n 0 ) b k+1 DTS[n a k+1 -x ]. Slowdown Rule: For k > 0, (Q 1 n a 1 ) b 2 (Q 2 n a 2 ) • • • b k-1 (Q k-1 n a k-1 ) b k DTS[n c•max{a k+1 ,a k ,b k ,b k+1 } ]. An alternation-trading proof shows (NTIME[n] ⊆ DTS[n c ] =⇒ A 1 ⊆ A 2 ) if its first line is A 1 and its last line is A 2 .
The above definition comes directly from the Speedup Lemma (Lemma 2.3) and Slowdown Lemma (Lemma 2.4). The rules are easily verified to be syntactic formulations of the corresponding lemmas. For instance, Speedup Rule 1 holds, as

(Q 1 n a 1 ) b 2 (Q 2 n a 2 ) • • • b k (Q k n a k ) b k+1 DTS[n a k+1 ] ⊆ (Q 1 n a 1 ) b 2 (Q 2 n a 2 ) • • • b k (Q k n a k ) b k+1 (Q k n x ) max{b k+1 ,x} (Q k+1 n 0 ) b k+1 DTS[n a k+1 ] ⊆ (Q 1 n a 1 ) b 2 (Q 2 n a 2 ) • • • b k (Q k n max{a k ,x} ) max{b k+1 ,x} (Q k+1 n 0 ) b k+1 DTS[n a k+1 ].
Rule 2 is akin to Rule 1, except that it uses opposite quantifiers in its invocation of the Speedup Lemma. The Slowdown Rule works analogously to Lemma 2.4. It follows that alternation-trading proofs are sound.

Note Speedup Rules 0 and 2 add two quantifier blocks, Speedup Rule 1 adds one quantifier, and all three rules introduce a parameter x. By considering "normal form" proofs (defined in the following paragraphs), we can prove that Rule 2 can always be replaced by applications of Rule 1. (A proof is in the full version of the paper.) For this reason we just refer to the Speedup Rule, depending on which of Rule 0 or Rule 1 applies.

Define a class of the form (3.1) to be simple. Define classes A 1 and A 2 to be complementary if A 1 is the class of complements of languages in A 2 . Every known (model-independent) time-space lower bound for SAT shows "NTIME[n] ⊆ DTS[n c ] implies A 1 ⊆ A 2 ", for some complementary simple classes A 1 and A 2 , contradicting a time hierarchy (cf. Theorem 2.5). A similar claim holds for nondeterministic time-space lower bounds against tautologies (which prove "NTIME

[n] ⊆ coNTS[n c ] implies A 1 ⊆ A 2 "), for d-dimensional TM lower bounds (which prove "NTIME[n] ⊆ DTIME d [n c ] implies A 1 ⊆ A 2 "
), and other problems. Normal Form. It will be very convenient to introduce a normal form for alternationtrading proofs. We show that any lower bound provable with complementary simple classes can also be established with a normal form proof. This greatly reduces the degrees of freedom in a proof, as we no longer need to worry about which time hierarchy to contradict.

Please note that the (k + 1)th quantifier is n 0 in order to account for the O(log n) size of the quantifier. Theorem 3.4. Let A 1 and A 2 be complementary. If there is an alternation-trading proof P for c that shows

(NTIME[n] ⊆ DTS[n c ] =⇒ A 1 ⊆ A 2 ),
then there is a normal form proof for c, of length at most that of P .

Proofs of Lemma 3.3 and Theorem 3.4 are in the full version. The upshot of these results is that we may focus our proof search on normal form proofs. For the remainder of this section, we assume all alternation-trading proofs are in normal form.

Proof Annotations. Different lower bound proofs can result in quite different sequences of speedups and slowdowns. A proof annotation represents such a sequence. Definition 3.5. A proof annotation for an alternation-trading proof of ℓ lines is the (ℓ -1)bit vector A where for all i = 1, . . . , ℓ -1, A[i] = 1 (respectively, A[i] = 0) if the ith line applies a Speedup Rule (respectively, a Slowdown Rule).

An (ℓ -1)-bit proof annotation corresponds to a "strategy" for an ℓ-line proof. For a normal form proof of ℓ lines, it is not hard to show that its annotation A must have

A[1] = 1, A[ℓ -2] = 0, and A[ℓ -1] = 0.
Note that an annotation does not determine a proof entirely, as other parameters need optimizing. (The problem of optimizing them is tackled in the next section.) To illustrate the annotation concept, we give four examples.

• The n √ 2 lower bound of Lipton and Viglas has the annotation [1, 0, 0].

• The n 1.6004 bound from Section 2.1 corresponds to [1, 1, 0, 0, 1, 0, 0]. • The n φ bound of Fortnow and Van Melkebeek [START_REF] Fortnow | Time-Space Tradeoffs for Nondeterministic Computation[END_REF] is an inductive proof, corresponding to an infinite sequence of annotations. In normal form, the sequence is [1, 0, 0], [1, 1, 0, 0, 0], [1, 1, 1, 0, 0, 0, 0], . . . • The n 2 cos(π/7) bound [START_REF] Williams | Time-space tradeoffs for counting NP solutions modulo integers[END_REF] has two inductive stages. Let A = 1, 0, 1, 0, . . . , 1, 0, 0, where the '. . .' contain any number of repetitions. The sequence is

[A], [1, A, A], [1, 1, A, A, A], [1, 1, 1, A, A, A, A],
. . . That is, the proof performs many speedups, then a sequence of many slowdownspeedup alternations, then two consecutive slowdowns, repeating this until all the quantifiers have been removed.

Translation To Linear Programming

Given a (normal form) proof annotation, how can we determine the best proof possible with it? We need to optimally set the runtimes of the first and last DTS classes in the proof, as well as the x i parameters that arise from each application of a Speedup Rule. It turns out that an annotation A and c > 1 can be reduced to a polynomial size linear program that is feasible if and only if there is an alternation-trading proof of NTIME[n] DTS[n c ] with annotation A. More precisely, the problem of optimizing parameters can be viewed as an arithmetic circuit evaluation, where the circuit has max gates, addition gates, and input gates that may multiply their input by c. Such circuits can be evaluated using a linear program that minimizes the sum of the gate values (cf. [START_REF] Derman | Finite state Markov decision processes[END_REF]).

Let A be an annotation of ℓ -1 bits, and let m be the maximum number of quantifier blocks in any line of A (note m is easily computed in linear time). The target LP has variables a i,j , b i,j , and x i , for all i = 0, . . . , ℓ -1 and j = 1, . . . , m. The variables a i,j represent the runtime exponent of the jth quantifier block in the class on the ith line, b i,j is the input exponent to the jth quantifier block of the class on the ith line, and for all lines i that use a Speedup Rule, x i is the choice of x in the Speedup Rule. For example:

• If the kth line of a proof is DTS[n a ], the corresponding constraints are a k,1 = a, b k,1 = 1, (∀k > 0) a k,i = b k,i = 0. • If the kth line of a proof is (∃ n a ′ ) b DTS[n a ], then the constraints are a k,0 = a, b k,1 = b, a k,1 = a ′ , b k,1 = 1, (∀k > 1) a k,i = b k,i = 0.
The objective is to minimize i,j (a i,j + b i,j ) + i x i . The LP constraints depend on the lines of the annotation, as follows.

Initial Constraints. For the 0th and (ℓ -1)th lines we have a 0,1 ≥ a ℓ-1,1 , and

a 0,1 ≥ 1, b 0,1 = 1, (∀ k > 1) a 0,k = b 0,k = 0, and a ℓ,1 ≥ 1, b ℓ,1 = 1, (∀k > 1) a ℓ,k = b ℓ,k = 0,
representing DTS[n a 0,1 ] and DTS[n a ℓ-1,0 ], respectively. The 1st line of a proof always applies Speedup Rule 1, having the form (Q

1 n x ) max{x,1} (Q 2 n 0 ) 1 DTS[n a-x ].
So the constraints for the 1st line are:

a 1,1 = a 0,1 -x 1 , b 1,1 = 1, a 1,2 = 0, b 1,2 ≥ x 1 , b 1,2 ≥ 1, a 1,3 = x 3 , b 1,3 = 1, (∀ k : 4 ≤ k ≤ m) a 1,k = b 1,k = 0.
The below constraint sets simulate the Speedup and Slowdown Rules:

Speedup Rule Constraints. For the ith line where i > 1 and A[i] = 1, we have

a i,1 ≥ 1, a i,1 ≥ a i-1,1 -x i , b i,1 = b i-1,1 , a i,2 = 0, b i,2 ≥ x i , b i,2 ≥ b i-1,1 , a i,3 ≥ a i-1,2 , a i,3 ≥ x i , b i,3 ≥ b i-1,2 , (∀ k : 4 ≤ k ≤ m) a i,k = a i-1,k-1 , b i,k = b i-1,k-1 . The constraints express that • • • b 2 (Q 2 n a 2 ) b 1 DTS[n a 1 ] in the (i -1)th line is replaced by • • • b 2 (Q 2 n max{a 2 ,x} ) max{x,b 1 } (Q 1 n 0 ) b 1 DTS[n max{a 1 -x,1} ] in the ith line, where Q 1 is opposite to Q 2 .
Slowdown Rule Constraints. For the ith line where A[i] = 0, the constraints are

a i,1 ≥ c • a i-1,1 , a i,1 ≥ c • a i-1,2 , a i,1 ≥ c • b i-1,1 , a i,1 ≥ c • b i-1,2 , b i,1 = b i-1,2 (∀ k : 2 ≤ k ≤ m -1) a i,k = a i-1,k+1 , b i,k = b i-1,k+1 , a i,m = b i,m = 0. These express the replacement of • • • b 2 (Q 1 n a 2 ) b 1 DTS[n a 1 ] in the (i -1)th line with • • • b 2 DTS[n c•max{a 1 ,a 2 ,b 1 ,b 2 } ]
in the ith line. This concludes the description of the linear program. To find the largest c that still yields a feasible LP, we can simply binary search for it. The following summarizes this section.

Theorem 3.6. Given an annotation of n lines, the best possible alternation-trading proof following the annotation can be determined up to n digits of precision, in poly(n) time.

Results

Following the above formulation, we wrote proof search routines in Maple. Many millions of proof annotations were tried, including all those corresponding to prior work, with no success beyond the 2 cos(π/7) exponent. The best lower bounds followed a highly regular pattern; see the full version for more on this. We are led to: Conjecture 3.7. There is no alternation-trading proof that NTIME[n] DTS[n c ] for all c > 2 cos(π/7).

Proving the conjecture seems currently out of reach. However, we can show: A proof is in the full version. At a high level, the proof argues that any minimum length proof of a quadratic lower bound could be shortened, giving a contradiction.

Despite this bad news, the theorem prover did provide enough insight to aid in a new lower bound of n 2 cos(π/7)-o(1) on the time-space product of any SAT algorithm. Theorem 3.9. Let t(n) and s(n) be bounded above by polynomials. Any algorithm solving SAT in time t and space s requires t • s = Ω(n 2 cos(π/7)-ε ) for all ε > 0.

These lower bounds have also been generalized to the QBF problem: Theorem 3.10. For all k ≥ 1, QBF k requires Ω(n c ) time on n o(1) space RAMs, where c 3 /k -c 2 -2c + k < 0.

Discussion

We introduced a methodology for reasoning about alternation-trading proofs of lower bounds. It provides a generic means for computers to help us attack lower bound problems, and lets us establish limitations on known techniques. We now have a better understanding of what these techniques can and cannot do, and a tool for addressing future problems. Previously, the problem of setting parameters to achieve a good lower bound was a highly technical exercise. Our work should facilitate further research: once a new speedup or slowdown lemma is found, one only needs to find the relevant linear programming formulation to begin understanding its power. We conclude with two open-ended problems.

(1) Establish tight limitations for alternation-trading proofs. That is, show that the best possible alternation-trading proofs match those we have provided. Our computer search results have been met with healthy skepticism. It is critical to verify these perceived limitations with formal proof. We have managed to prove non-trivial limitations; it is possible that the ideas in those can be extended. (2) Discover new ingredients to add to the framework. One possibility is to find new separation results that lead to new contradictions. Another is to find improved Speedup and/or Slowdown Lemmas. The Slowdown Lemmas are the "blandest" of the ingredients, in that they are the most elementary (and they relativize).

  4 /2 ] (Slowdown) When c 2 /2 + 2 > c 4 /2 (which happens if c < 1.6004), we have DTS[n a ] ⊆ DTS[n a ′ ] for some a > a ′ . One can show by a translation argument (similar to the footnote) that either DTS[n a ] DTS[n a ′ ] or NTIME[n] DTS[n c ], concluding the proof.

Definition 3. 2 .

 2 Let c ≥ 1. An alternation-trading proof for c is in normal form if (a) the first and last lines are DTS[n a ] and DTS[n a ′ ] respectively, for some a ≥ a ′ , and (b) no other lines are DTS classes. We show that a normal form proof for c implies that NTIME[n] DTS[n c ]. Lemma 3.3. Let c ≥ 1. If there is an alternation-trading proof for c in normal form having at least two lines, then NTIME[n] DTS[n c ].

Theorem 3. 8 .

 8 There is no alternation-trading proof that NTIME[n] DTS[n 2 ].

  contradicts Theorem 2.5. In fact, one can show that if c 2 = 2, we still have a contradiction with NTIME[n] ⊆ DTS[n c ], so the ε can be removed from the previous statement and state that SAT cannot be solved in n

	√ 2 time and n o(1) exactly. §
	(2) Improving on the previous example, one can show SAT / ∈ DTS[n 1.6004 ]. If NTIME[n] ⊆ DTS[n c ] and √ 2 ≤ c < 2, then applying the Speedup and Slowdown Lemmas one can derive:

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copy of this license, visit http://creativecommons.org/licenses/by-nd/3.0/.

Acknowledgements. I am grateful to my thesis committee for their invaluable feedback on my PhD thesis, which included preliminary results on this work. Thanks to Scott Aaronson for useful discussions about irrelativization, and thanks to the STACS referees for very thoughtful comments.

This material is based on work supported in part by NSF grant CCR-0122581 while the author was a student at Carnegie Mellon University, and NSF grant CCF-0832797 while the author was a member of the Institute for Advanced Study. c R. R. Williams

CC