From Small Space to Small Width in Resolution

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

doi:10.4230/LIPIcs.STACS.2014.300

Document

From Small Space to Small Width in Resolution

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

Part of: Volume: 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: Symposium on Theoretical Aspects of Computer Science (STACS)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2014-03-05

PDF

File

PDF

LIPIcs.STACS.2014.300.pdf

Filesize: 0.55 MB
12 pages

Document Identifiers

DOI: 10.4230/LIPIcs.STACS.2014.300
URN: urn:nbn:de:0030-drops-44661

Subject Classification

Keywords

proof complexity
resolution
width
space
polynomial calculus
PCR

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get BibTex

Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, and Marc Vinyals. From Small Space to Small Width in Resolution. In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 25, pp. 300-311, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/LIPIcs.STACS.2014.300

Author Details

Yuval Filmus

Massimo Lauria

Mladen Miksa

Jakob Nordström

Marc Vinyals

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail