From small space to small width in resolution

Forskningsoutput: Kapitel i bok/rapport/Conference proceedingKonferenspaper i proceeding

Abstract

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.

Detaljer

Författare
Externa organisationer
  • University of California, Berkeley
  • KTH Royal Institute of Technology
Forskningsområden

Ämnesklassifikation (UKÄ) – OBLIGATORISK

  • Algebra och logik
  • Datavetenskap (datalogi)

Nyckelord

Originalspråkengelska
Titel på värdpublikation31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014
RedaktörerNatacha Portier, Ernst W. Mayr
FörlagSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Sidor300-311
Antal sidor12
Volym25
ISBN (elektroniskt)9783939897651
StatusPublished - 2014 mar 1
PublikationskategoriForskning
Peer review utfördJa
Externt publiceradJa
Evenemang31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014 - Lyon, Frankrike
Varaktighet: 2014 mar 52014 mar 8

Publikationsserier

NamnLeibniz International Proceedings in Informatics, LIPIcs
FörlagSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volym25
ISSN (tryckt)1868-8969

Konferens

Konferens31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014
LandFrankrike
OrtLyon
Period2014/03/052014/03/08