|
Speaker: Chris Beck
Princeton University
Title: Time Space Tradeoffs in Proof Complexity
Abstract:
For modern SAT solvers based on DPLL with clause learning, the two major bottlenecks are the time and memory used by the algorithm. This raises the question of whether this memory bottleneck is inherent to Resolution based approaches, or an artifact of the particular search heuristics currently used in practice? There is a well known correspondence between these algorithms and the Resolution proof system, in which these resources correspond to the length and space of proofs. While every tautology has a linear-space proof, this proof is in general of exponential size, raising the issue of size-space tradeoffs: perhaps, in high space, there is a short proof, but with constrained space only much longer proofs exist. Space complexity and time-space tradeoffs have been the subject of much recent work in proof complexity, but until our recent work no such bound applied to super-linear amounts of space. In recent work with Paul Beame and Russell Impagliazzo, we obtained strong time-space tradeoff lower bounds beyond the linear space threshold -- for instance, for each k, we give a sequence of formulas with a polynomial size proof using space n^k, but for which any proof in space n^{k/2} has superpolynomial size. Thus, on these instances, if you want to run in polynomial time, you need a large polynomial amount of space. In fact we obtain formulas at all level of hardness for which the proof space must be within a polynomial factor of the optimal proof size, or else the proof size blows up quasipolynomially.
This result was recently simplified and extended in work of myself, Jakob Nordstr{\"o}m, and Bangsheng Tang; among other results, we obtain these same tradeoffs in Polynomial Calculus Resolution. Polynomial Calculus Resolution is an extension of Resolution relevant to algebraic SAT solvers based on Gr{\"o}bner basis methods; our results imply that there are some formulas whose time space tradeoff characteristics are not significantly improved by adding algebraic reasoning on top of resolution in this way. In this talk, I will discuss in detail the simplified proof for Resolution and sketch the proof for Polynomial Calculus.
|