From small space to small width in resolution

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation-previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.

Original languageEnglish
Title of host publication31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014
EditorsNatacha Portier, Ernst W. Mayr
Number of pages12
Volume25
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication date1 Mar 2014
Pages300-311
ISBN (Electronic)9783939897651
DOIs
Publication statusPublished - 1 Mar 2014
Externally publishedYes
Event31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014 - Lyon, France
Duration: 5 Mar 20148 Mar 2014

Conference

Conference31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014
LandFrance
ByLyon
Periode05/03/201408/03/2014

    Research areas

  • PCR, Polynomial calculus, Proof complexity, Resolution, Space, Width

ID: 251869919