期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2009
卷号：2009
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：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.
关键词：lower bound , pebble game , pebbling formula , Proof Complexity , Resolution , separation , size , Space , trade-off
