  Most state-of-the-art satisfiability algorithms today are variants of the
DPLL procedure augmented with clause learning. The main bottleneck for such
algorithms, other than the obvious one of time, is the amount of memory used.
In the field of proof complexity, the resources of time and memory correspond
to the length and space of resolution proofs. There has been a long line of
research trying to understand these proof complexity measures, but while strong
results have been proven on length our understanding of space is still quite
poor. For instance, it remains open whether the fact that a formula is provable
in short length implies that it is also provable in small space or whether on
the contrary these measures are unrelated in the sense that short proofs can be
arbitrarily complex with respect to space.
  In this paper, we present some evidence that the true answer should be that
the latter case holds. We do this by proving a tight bound of Theta(sqrt(n)) on
the space needed for so-called pebbling contradictions over pyramid graphs of
size n. This yields the first polynomial lower bound on space that is not a
consequence of a corresponding lower bound on width, another well-studied
measure in resolution, as well as an improvement of the weak separation in
(Nordstrom 2006) of space and width from logarithmic to polynomial.
  Also, continuing the line of research initiated by (Ben-Sasson 2002) into
trade-offs between different proof complexity measures, we present a simplified
proof of the recent length-space trade-off result in (Hertel and Pitassi 2007),
and show how our ideas can be used to prove a couple of other exponential
trade-offs in resolution.
