Chris Beck will present his preFPO on Friday Jan 31 at 3PM in Room 402. Everyone is invited to attend his talk. His abstract follows below. ----- Original Message ----- Title: Lower Bounds for Time and Space In this thesis we study the computational limitations of restricted models of computation. We pay particular attention to ``simple'' algorithms for satisfiability, that is, algorithms which are permitted to use large amounts of traditional resources such as space and time, but whose correctness must be provable in a simple proof system. This has the consequence that when an algorithm accepts or rejects an input, the computation history corresponds to a simple propositional proof of the input's status, and that studying the structure of such proofs allows us to formally understand some of the difficulties faced by the algorithm. The fact that many algorithms yield proofs has been observed in a variety of scenarios in both theory and practice. Moreover, in many of these cases, proof complexity is the only known way to analyze the running time of such algorithms.
From a different point of view, our results are interesting because the techniques for proof lower bounds are closely related to the known techniques for circuit lower bounds. Lower bounds for circuits via random restrictions and via Razoborv's method of approximations are closely related to Haken's bottleneck counting method for Resolution lower bounds, and well-known work of Beame et al. shows that this analogy can be carried through even for AC0 Frege proofs.
One of our most important contributions to the area is to show that the bottleneck counting technique can also be used to show time space trade-offs. Indeed, while previous time space tradeoffs used ad-hoc techniques and only applied in the sublinear space regime, we show that the same technique which gives (tight) proof size lower bounds can be vastly generalized to yield superpolynomial time space tradeoffs which are tight in the high space regime. It is an interesting question for future research whether our technique could also be used for restricted circuits, such as monotone circuits, or in a model such as read once algebraic branching programs. Our results are the following: - We give the first time space trade-off results for Resolution which are meaningful in the regime of {\emph{ superlinear}} space. More concretely, we give tautologies which have polynomial size resolution proofs which may be carried out in polynomial space (and which standard algorithms would find in polynomial time using polynomial memory), but for which even slightly reduced space entails a superpolynomial size resolution proof. This gives the first formal explanation for why DPLL+Clause Learning SAT solvers need a large amount of space to work well in practice, and gives evidence to support the main conjecture of Allender et al. (2012) regarding tree-width parameterized satisfiability. - We extend these techniques to the stronger Polynomial Calculus Resolution proof system, an algebraic system used sometimes in practice instead of traditional SAT solvers, based on Grobner Basis techniques. - We show that the Strong Exponential Time Hypothesis applies to the proof system of regular resolution, and thus to algorithms based on the original Davis Putnam procedure. We conjecture that SETH holds for general resolution, and improve the state of the art size lower bounds for resolution proofs. In particular, we show that Grover's black box search algorithm solves SAT faster than any classical SAT solver. - We expand upon recent work of Lovett and Viola, giving an explicit distribution of strings which is hard to approximately sample in AC0. Our results are essentially best possible in terms of the size of the circuits and quality of the approximation. In addition we prove a new concentration bound for collections of decision trees, and a structure theorem for these, which could be useful in future applications.