Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
From small space to small width in resolution
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.ORCID-id: 0000-0003-4003-3168
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.ORCID-id: 0000-0002-2700-4285
Visa övriga samt affilieringar
2014 (Engelska)Ingår i: 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2014, Vol. 25, s. 300-311Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2014. Vol. 25, s. 300-311
Serie
Leibniz International Proceedings in Informatics, LIPIcs, ISSN 1868-8969 ; 25
Nyckelord [en]
PCR, Polynomial calculus, Proof complexity, Resolution, Space, Width
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
URN: urn:nbn:se:kth:diva-158079DOI: 10.4230/LIPIcs.STACS.2014.300Scopus ID: 2-s2.0-84907818998ISBN: 978-393989765-1 (tryckt)OAI: oai:DiVA.org:kth-158079DiVA, id: diva2:774286
Konferens
31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, Lyon, France, 5 March 2014 through 8 March 2014
Anmärkning

QC 20141222

Tillgänglig från: 2014-12-22 Skapad: 2014-12-22 Senast uppdaterad: 2018-01-11Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Personposter BETA

Lauria, MassimoNordström, JakobVinyals, Marc

Sök vidare i DiVA

Av författaren/redaktören
Lauria, MassimoMikša, MladenNordström, JakobVinyals, Marc
Av organisationen
Teoretisk datalogi, TCS
Data- och informationsvetenskap

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 33 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf