Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
From small space to small width in resolution
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0003-4003-3168
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
Show others and affiliations
2014 (English)In: 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2014, Vol. 25, 300-311 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2014. Vol. 25, 300-311 p.
Series
Leibniz International Proceedings in Informatics, LIPIcs, ISSN 1868-8969 ; 25
Keyword [en]
PCR, Polynomial calculus, Proof complexity, Resolution, Space, Width
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-158079DOI: 10.4230/LIPIcs.STACS.2014.300Scopus ID: 2-s2.0-84907818998ISBN: 978-393989765-1 (print)OAI: oai:DiVA.org:kth-158079DiVA: diva2:774286
Conference
31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, Lyon, France, 5 March 2014 through 8 March 2014
Note

QC 20141222

Available from: 2014-12-22 Created: 2014-12-22 Last updated: 2014-12-22Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Lauria, MassimoNordström, JakobVinyals, Marc

Search in DiVA

By author/editor
Lauria, MassimoMikša, MladenNordström, JakobVinyals, Marc
By organisation
Theoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 28 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf