TR08-026 Authors: Jakob NordstrÃ¶m, Johan Hastad

Publication: 12th March 2008 10:08

Downloads: 1373

Keywords:

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.