Paper Info
Title
Understanding space in resolution: optimal lower bounds and exponential trade-offs.
Abstract
For current state-of-the-art satisfiability algorithms ba sed on the DPLL procedure and clause learn- ing, 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, thes e resources correspond to the length and space of resolution proofs for formulas in conjunctive normal form (CNF). There has been a long line of re- search 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 r estrictions. In this paper, we remedy this situation by proving a host of length-space trade-off results for reso- lution in a completely general setting. Our collection of tr ade-offs cover space ranging over the whole interval from constant to O(n/loglogn), and most of them are superpolynomial or even exponential. Our key technical contribution is the following, somewhat surprising, theorem: Any CNF formulaF can be transformed by simple substitution into a new formula F 0 such that if F has the right properties, F 0 can be proven in essentially the same length as F while the minimal space needed for F 0 is lower- bounded by the number of variables mentioned simultaneously in any proof forF . Applying this theorem to so-called pebbling formulas defined in terms of pebble gam es 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.
Year
Venue
Keywords
2009
Electronic Colloquium on Computational Complexity (ECCC)
proof complexity,conjunctive normal form,covering space,computer science,lower bound,directed acyclic graph,limit set,satisfiability
DocType
Volume
Citations 
Journal
16
5
PageRank 
References 
Authors
0.41
49
2
Name
Order
Citations
PageRank
Eli Ben-Sasson1164186.98
Jakob Nordström217721.76