License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2014.300
URN: urn:nbn:de:0030-drops-44661
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4466/
Go to the corresponding LIPIcs Volume Portal

Filmus, Yuval ; Lauria, Massimo ; Miksa, Mladen ; Nordström, Jakob ; Vinyals, Marc

From Small Space to Small Width in Resolution

pdf-format:
24.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{filmus_et_al:LIPIcs:2014:4466,
  author =	{Yuval Filmus and Massimo Lauria and Mladen Miksa and Jakob Nordstr{\"o}m and Marc Vinyals},
  title =	{{From Small Space to Small Width in Resolution}},
  booktitle =	{31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)},
  pages =	{300--311},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-65-1},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{25},
  editor =	{Ernst W. Mayr and Natacha Portier},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4466},
  URN =		{urn:nbn:de:0030-drops-44661},
  doi =		{10.4230/LIPIcs.STACS.2014.300},
  annote =	{Keywords: proof complexity, resolution, width, space, polynomial calculus, PCR}
}

Keywords: proof complexity, resolution, width, space, polynomial calculus, PCR
Collection: 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)
Issue Date: 2014
Date of publication: 05.03.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI