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, as well as relating them to the width
of proofs, i.e., the size of the largest clause in the proof, which
has been shown to be intimately connected with both length and space.
While strong results have been proven for length and width, our
understanding of space is still quite poor. For instance, it has
remained open whether the fact that a formula is provable in short
length implies that it is also provable in small space (which is the
case for length versus width), or whether on the contrary these
measures are completely 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 and provide a possible roadmap for how such
an optimal separation result could be obtained. 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, as well as an improvement of the
weak separation of space and width in (Nordström 2006) 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.