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
Narrow proofs may be spacious: Separating space and width in resolution
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
2006 (English)In: Proc. Annu. ACM Symp. Theory Comput., 2006, 507-516 p.Conference paper, Published paper (Refereed)
Abstract [en]

The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is the maximal number of clauses kept in memory simultaneously if the proof is only allowed to infer new clauses from clauses currently in memory. Both of these measures have previously been studied and related to the resolution refutation size of unsatisfiable CNF formulas. Also, the refutation space of a formula has been proven to be at least as large as the refutation width, but it has been open whether space can be separated from width or the two measures coincide asymptotically. We prove that there is a family of k-CNF formulas for which the refutation width in resolution is constant but the refutation space is non-constant, thus solving a problem mentioned in several previous papers.

Place, publisher, year, edition, pages
2006. 507-516 p.
Series
Proceedings of the Annual ACM Symposium on Theory of Computing, ISSN 0737-8017 ; 2006
Keyword [en]
Lower bound, Pebble game, Pebbling contradiction, Proof complexity, Resolution, Separation, Space, Width, Mathematical models, Set theory, Graph theory
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-155996Scopus ID: 2-s2.0-33748114893ISBN: 1595931341 (print)ISBN: 9781595931344 (print)OAI: oai:DiVA.org:kth-155996DiVA: diva2:765805
Conference
38th Annual ACM Symposium on Theory of Computing, STOC'06, 21-23 May 2006, Seattle, WA, USA
Note

QC 20141125

Available from: 2014-11-25 Created: 2014-11-17 Last updated: 2014-11-25Bibliographically approved

Open Access in DiVA

No full text

Scopus

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

isbn
urn-nbn

Altmetric score

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