Computer Science/Discrete Mathematics Seminar II

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? 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 this work, no such bound applied to super-linear amounts of space. We obtain strong time space tradeoff lower bounds for a simple and explicit collection of formulas -- in particular for any k, we give a sequence of formulas of length n such that with n^k space there is a proof of length polynomial in n, but for which every proof is superpolynomial when the space is constrained to n^{k/2}. Thus, on these instances, if you want to run in polynomial time, you need a large polynomial amount of space. Joint work with Paul Beame and Russell Impagliazzo