From small space to small width in resolution

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Standard

From small space to small width in resolution. / Filmus, Yuval; Lauria, Massimo; Mikša, Mladen; Nordström, Jakob; Vinyals, Marc.

31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014. ed. / Natacha Portier; Ernst W. Mayr. Vol. 25 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2014. p. 300-311.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Harvard

Filmus, Y, Lauria, M, Mikša, M, Nordström, J & Vinyals, M 2014, From small space to small width in resolution. in N Portier & EW Mayr (eds), 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014. vol. 25, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 300-311, 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, Lyon, France, 05/03/2014. https://doi.org/10.4230/LIPIcs.STACS.2014.300

APA

Filmus, Y., Lauria, M., Mikša, M., Nordström, J., & Vinyals, M. (2014). From small space to small width in resolution. In N. Portier, & E. W. Mayr (Eds.), 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014 (Vol. 25, pp. 300-311). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.STACS.2014.300

Vancouver

Filmus Y, Lauria M, Mikša M, Nordström J, Vinyals M. From small space to small width in resolution. In Portier N, Mayr EW, editors, 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014. Vol. 25. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2014. p. 300-311 https://doi.org/10.4230/LIPIcs.STACS.2014.300

Author

Filmus, Yuval ; Lauria, Massimo ; Mikša, Mladen ; Nordström, Jakob ; Vinyals, Marc. / From small space to small width in resolution. 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014. editor / Natacha Portier ; Ernst W. Mayr. Vol. 25 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2014. pp. 300-311

Bibtex

@inproceedings{49e1bd85dd1242aab37967f482531272,
title = "From small space to small width in resolution",
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.",
keywords = "PCR, Polynomial calculus, Proof complexity, Resolution, Space, Width",
author = "Yuval Filmus and Massimo Lauria and Mladen Mik{\v s}a and Jakob Nordstr{\"o}m and Marc Vinyals",
year = "2014",
month = mar,
day = "1",
doi = "10.4230/LIPIcs.STACS.2014.300",
language = "English",
volume = "25",
pages = "300--311",
editor = "Natacha Portier and Mayr, {Ernst W.}",
booktitle = "31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
note = "31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014 ; Conference date: 05-03-2014 Through 08-03-2014",

}

RIS

TY - GEN

T1 - From small space to small width in resolution

AU - Filmus, Yuval

AU - Lauria, Massimo

AU - Mikša, Mladen

AU - Nordström, Jakob

AU - Vinyals, Marc

PY - 2014/3/1

Y1 - 2014/3/1

N2 - 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.

AB - 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.

KW - PCR

KW - Polynomial calculus

KW - Proof complexity

KW - Resolution

KW - Space

KW - Width

UR - http://www.scopus.com/inward/record.url?scp=84907818998&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.STACS.2014.300

DO - 10.4230/LIPIcs.STACS.2014.300

M3 - Article in proceedings

AN - SCOPUS:84907818998

VL - 25

SP - 300

EP - 311

BT - 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014

A2 - Portier, Natacha

A2 - Mayr, Ernst W.

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014

Y2 - 5 March 2014 through 8 March 2014

ER -

ID: 251869919