For modern SAT solvers based on DPLL with clause learning, the two major bottlenecks are the time and memory used by the algorithm. 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. Much recent research in proof complexity has focused on understanding this memory bottleneck -- is it inherent to the Resolution based approach, or is it an artifact of the search heuristics used in practice? The most direct approach to this question would be to try to prove unconditional space lower bounds for proofs of some particular formula, but this approach is limited by the observation that every formula has a trivial proof which may be carried out in space no larger than the size of the formula. The catch is that this proof is exponentially large in general, so a natural next step is to try to show that for some formula, such a penalty must be incurred when the space is thus constrained. This is formalized by a tradeoff result -- in high space, there is a short proof, but with constrained space only much longer proofs exist.

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. Previous research has only been able to obtain tradeoffs when the space is sublinear. This is the first result that has allowed us to distinguish the efficiency of e.g. Resolution with linear space versus quadratic space.