Theory of Computing
-------------------
Title : Towards an Optimal Separation of Space and Length in Resolution
Authors : Jakob Nordstrom and Johan Haastad
Volume : 9
Number : 14
Pages : 471-557
URL : https://theoryofcomputing.org/articles/v009a014
Abstract
--------
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 a 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 has been 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 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 indicating that the latter case
should hold and provide a roadmap for how such an optimal separation
result could be obtained. We do so 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 of Nordstr\"{o}m (STOC 2006) from
logarithmic to polynomial.
A preliminary version (http://dx.doi.org/10.1145/1374376.1374478) of
this paper appeared in the Proceedings of the 40th Annual ACM
Symposium on Theory of Computing (STOC'08).