Change search
ReferencesLink to record
Permanent link

Direct link
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
2009 (English)In: SIAM journal on computing (Print), ISSN 0097-5397, E-ISSN 1095-7111, Vol. 39, no 1, 59-121 p.Article in journal (Refereed) Published
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 conjunctive normal form (CNF) formulas. Also, the minimum refutation space of a formula has been proven to be at least as large as the minimum 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 nonconstant, thus solving a problem mentioned in several previous papers.

Place, publisher, year, edition, pages
2009. Vol. 39, no 1, 59-121 p.
Keyword [en]
proof complexity, resolution, width, space, separation, lower bound, pebble game, pebbling contradiction
National Category
Computer Science
URN: urn:nbn:se:kth:diva-30799DOI: 10.1137/060668250ISI: 000267744400004ScopusID: 2-s2.0-67650162541OAI: diva2:403460
QC 20110314Available from: 2011-03-14 Created: 2011-03-04 Last updated: 2012-01-23Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Nordström, Jakob
By organisation
Theoretical Computer Science, TCS
In the same journal
SIAM journal on computing (Print)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 19 hits
ReferencesLink to record
Permanent link

Direct link