Change search
ReferencesLink to record
Permanent link

Direct link
Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
2010 (English)Conference paper (Refereed)
Abstract [en]

For current state-of-the-art satisfiability algorithms based on the DPLL procedure and clause learning, the tw main bottlenecks are the amounts of time and memory used. 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 restricted settings. 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 almost the whole range of values for the space complexity of formulas, and most of the trade-offs are superpolynomial or even exponential and essentially tight. Using similar techniques, we show that these trade-offs in fact extend (albeit with worse parameters) to the exponentially stronger k -DNF resolution proof systems, which operate with formulas in disjunctive normal form with terms of bounded arity k . We also answer the open question whether the k -DNF resolution systems form a strict hierarchy with respect to space in the affirmative. Our key technical contribution is the following, somewhat surprising, theorem: Any CNF formula F can be transformed by simple variable substitution into a new formula F0such that ifF has the right properties, F0can be proven in essentially the same length asF , whereas on the other hand the minimal number of linesone needs to keep in memory simultaneously in any proof off is lower-bounded by the minimal number of variablesneeded simultaneously in any proof off Applying this theorem to so-called pebbling formulas defined in terms of pebble games on directed acyclic graphs, we obtain our results.

Place, publisher, year, edition, pages
National Category
Computer and Information Science
URN: urn:nbn:se:kth:diva-63126OAI: diva2:481661
Propositional Proof Complexity: Theory and Practice workshop at FLoC '10. Edinburgh, 9-21 July 2010
QC 20120123Available from: 2012-01-21 Created: 2012-01-21 Last updated: 2012-01-23Bibliographically approved

Open Access in DiVA

No full text

Search in DiVA

By author/editor
Nordström, Jakob
By organisation
Theoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 21 hits
ReferencesLink to record
Permanent link

Direct link