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 lenght 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), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-5379-345X
2013 (English)In: Theory of Computing, ISSN 1557-2862, E-ISSN 1557-2862, Vol. 9, 471-557 p.Article in journal (Refereed) Published
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 a 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 has been 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 these measures are unrelated in the sense that short proofs can be arbitrarily complex with respect to space.

In this paper, we present some evidence indicating that the latter case should hold and provide a roadmap for how such an optimal separation result could be obtained. We do so by proving a tight bound of Θ(n√) on the space needed for so-called pebbling contradictions over pyramid graphs of size n. This yields the first polynomial lower bound on space that is not a consequence of a corresponding lower bound on width, as well as an improvement of the weak separation of space and width of Nordström (STOC 2006) from logarithmic to polynomial.

Place, publisher, year, edition, pages
2013. Vol. 9, 471-557 p.
Keyword [en]
proof complexity, resolution, length, space, width, separation, lower bound, pebbling, black-white pebble game
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:kth:diva-138562DOI: 10.4086/toc.2013.v009a014OAI: oai:DiVA.org:kth-138562DiVA: diva2:681387
Note

QC 20140204

Available from: 2013-12-19 Created: 2013-12-19 Last updated: 2017-12-06Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Nordström, JakobHåstad, Johan

Search in DiVA

By author/editor
Nordström, JakobHåstad, Johan
By organisation
Theoretical Computer Science, TCS
In the same journal
Theory of Computing
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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