Speaker
Jakob Nordström
(KTH)
Description
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 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 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 talk, we present evidence that the true answer should be that the latter case holds and provide a roadmap for how such an optimal separation result could be obtained. We do this by proving a tight bound of Omega(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 (Nordström 2006) of space and width from logarithmic to polynomial.
Joint work with Johan Håstad, Royal Institute of Technology.
In this talk, we present evidence that the true answer should be that the latter case holds and provide a roadmap for how such an optimal separation result could be obtained. We do this by proving a tight bound of Omega(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 (Nordström 2006) of space and width from logarithmic to polynomial.
Joint work with Johan Håstad, Royal Institute of Technology.
