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
Towards an Optimal Separation of Space and Length in Resolution
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
KTH, School of Computer Science and Communication (CSC), Numerical Analysis and Computer Science, NADA.ORCID iD: 0000-0002-5379-345X
2008 (English)In: STOC'08: PROCEEDINGS OF THE 2008 ACM INTERNATIONAL SYMPOSIUM ON THEORY OF COMPUTING, NEW YORK: ASSOC COMPUTING MACHINERY , 2008, 701-710 p.Conference paper, Published paper (Refereed)
Abstract [en]

Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The main bottleneck for such algorithms, other than the obvious one of time, is the amount of memory used. In the field of proof complexity, the resources of time and memory correspond to the length and space of resolution proofs. There has been a long line of research trying to understand these proof complexity measures, as well as relating them to the width of proofs, i.e., the size of the largest clause in the proof, which has been shown to be intimately connected with both length and space. While strong results have been proven for length and width, our understanding of space is still quite poor. For instance, it has remained open whether the fact that a formula is provable in short length implies that it is also provable in small space (which is the case for length versus width), or whether on the contrary these measures are completely unrelated in the sense that short proofs can be arbitrarily complex with respect to space. In this paper, we present some evidence that the true answer should be that the latter case holds and provide a possible roadmap, for how such art optimal separation result could be obtained. We do this by proving a tight bound of Theta(root n)) on the space needed for so-called pebbling contradictions over pyramid graphs of size n. Also, continuing the line of research initiated by (Ben-Sasson 2002) into trade-offs between different proof complexity measures, we present a simplified proof of the recent length-space trade-off result in (Hertel and Pitassi 2007), and show how our ideas can be used to prove a couple of other exponential trade-offs in resolution.

Place, publisher, year, edition, pages
NEW YORK: ASSOC COMPUTING MACHINERY , 2008. 701-710 p.
Keyword [en]
Proof complexity, resolution, length, space, separation, lower bound, pebbling
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-30832DOI: 10.1145/1374376.1374478ISI: 000266622800076Scopus ID: 2-s2.0-57049099276ISBN: 978-1-60558-047-0 (print)OAI: oai:DiVA.org:kth-30832DiVA: diva2:403027
Conference
14th Annual ACM International Symposium on Theory of Computing Victoria, CANADA, MAY 17-20, 2008
Note

QC 20110310

Available from: 2011-03-10 Created: 2011-03-04 Last updated: 2012-09-25Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Nordström, JakobHåstad, Johan

Search in DiVA

By author/editor
Nordström, JakobHåstad, Johan
By organisation
Theoretical Computer Science, TCSNumerical Analysis and Computer Science, NADA
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 31 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