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.
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.
