From small space to small width in resolution

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

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.

OriginalsprogEngelsk
Titel31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014
RedaktørerNatacha Portier, Ernst W. Mayr
Antal sider12
Vol/bind25
ForlagSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publikationsdato1 mar. 2014
Sider300-311
ISBN (Elektronisk)9783939897651
DOI
StatusUdgivet - 1 mar. 2014
Eksternt udgivetJa
Begivenhed31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014 - Lyon, Frankrig
Varighed: 5 mar. 20148 mar. 2014

Konference

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

ID: 251869919