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
Short proofs may be spacious: 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
2008 (English)In: Proc. Annu. IEEE Symp. Found. Comput. Sci. FOCS, 2008, 709-718 p.Conference paper, Published paper (Refereed)
Abstract [en]

A number of works have looked at the relationship between length and space of resolution proofs. A notorious question has been whether the existence of a short proof implies the existence of a proof that can be verified using limited space. In this paper we resolve the question by answering it negatively in the strongest possible way. We show that there are families of 6-CNF formulas of size n, for arbitrarily large n, that have resolution proofs of length O(n) but for which any proof requires space Ω(n/log n). This is the strongest asymptotic separation possible since any proof of length O(n) can always be transformed into a proof in space O(n/log n). Our result follows by reducing the space complexity of so called pebbling formulas over a directed acyclic graph to the black-white pebbling price of the graph. The proof is somewhat simpler than previous results (in particular, those reported in [Nordström 2006, Nordström and Håstad 2008]) as it uses a slightly different flavor of pebbling formulas which allows for a rather straightforward reduction of proof space to standard black-white pebbling price.

Place, publisher, year, edition, pages
2008. 709-718 p.
Series
Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS, ISSN 0272-5428
Keyword [en]
Computers, Fiber optic chemical sensors, Cnf formulas, Directed Acyclic graphs, Large N, Limited spaces, Resolution proofs, Space complexities, Computational geometry
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-154144DOI: 10.1109/FOCS.2008.42ISI: 000262484800071Scopus ID: 2-s2.0-57949109817ISBN: 9780769534367 (print)OAI: oai:DiVA.org:kth-154144DiVA: diva2:756469
Conference
49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008, 25 October 2008 through 28 October 2008, Philadelphia, PA
Note

QC 20141017

Available from: 2014-10-17 Created: 2014-10-14 Last updated: 2015-10-06Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Nordström, Jakob

Search in DiVA

By author/editor
Nordström, Jakob
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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