Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR09-034 | 25th March 2009 00:00

Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs


Authors: Eli Ben-Sasson, Jakob Nordström
Publication: 18th April 2009 23:36
Downloads: 3685


For current state-of-the-art satisfiability algorithms based on the
DPLL procedure and clause learning, the two main bottlenecks are the
amounts of time and memory used. Understanding time and memory
consumption, and how they are related to one another, is therefore a
question of considerable practical importance. In the field of proof
complexity, these resources correspond to the length and space of
resolution proofs for formulas in conjunctive normal form (CNF).
There has been a long line of research investigating these proof
complexity measures, but while strong results have been established
for length, our understanding of space and how it relates to length
has remained quite poor. In particular, the question whether
resolution proofs can be optimized for length and space
simultaneously, or whether there are trade-offs between these two
measures, has remained essentially open apart from a few results in
very limited settings suffering from various technical restrictions.

In this paper, we remedy this situation by proving a host of
length-space trade-off results for resolution in a completely general
setting. Our collection of trade-offs cover space ranging over the
whole interval from constant to O(n/log n), and most of them are
superpolynomial or even exponential.

Our key technical contribution is the following, somewhat surprising,
theorem: Any CNF formula F can be transformed by simple substitution
into a new formula F' such that if F has the right properties, F' can
be proven in essentially the same length as F while the minimal space
needed for F' is lower-bounded by the number of variables mentioned
simultaneously in any proof for F. Applying this theorem to so-called
pebbling formulas defined in terms of pebble games on directed acyclic
graphs, and then using known results from the pebbling literature as
well as a proving a couple of new ones, we obtain our resolution
trade-off theorems.


Comment #1 to TR09-034 | 11th August 2010 18:58

This report has been subsumed

Comment #1
Authors: Eli Ben-Sasson, Jakob Nordström
Accepted on: 11th August 2010 18:58
Downloads: 3372


We have merged and updated our two ECCC technical reports TR09-034 and TR09-047, and published them as a new ECCC report TR10-125. (An identical version of the new report has also been posted to ArXiv.)

This new paper subsumes the previous two papers.

ISSN 1433-8092 | Imprint