Narrow proofs may be spacious: Separating space and width in resolution

Research output: Contribution to journal › Journal article › Research › peer-review

Standard

Narrow proofs may be spacious : Separating space and width in resolution. / Nordström, Jakob.

In: SIAM Journal on Computing, Vol. 39, No. 1, 2009, p. 59-121.

Research output: Contribution to journal › Journal article › Research › peer-review

Harvard

Nordström, J 2009, 'Narrow proofs may be spacious: Separating space and width in resolution', SIAM Journal on Computing, vol. 39, no. 1, pp. 59-121. https://doi.org/10.1137/060668250

APA

Nordström, J. (2009). Narrow proofs may be spacious: Separating space and width in resolution. SIAM Journal on Computing, 39(1), 59-121. https://doi.org/10.1137/060668250

Vancouver

Nordström J. Narrow proofs may be spacious: Separating space and width in resolution. SIAM Journal on Computing. 2009;39(1):59-121. https://doi.org/10.1137/060668250

Author

Nordström, Jakob. / Narrow proofs may be spacious : Separating space and width in resolution. In: SIAM Journal on Computing. 2009 ; Vol. 39, No. 1. pp. 59-121.

Bibtex

@article{be6de7d8925a4a5caa7fa113b7b79993,
title = "Narrow proofs may be spacious: Separating space and width in resolution",
abstract = "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.",
keywords = "Lower bound, Pebble game, Pebbling contradiction, Proof complexity, Resolution, Separation, Space, Width",
author = "Jakob Nordstr{\"o}m",
year = "2009",
doi = "10.1137/060668250",
language = "English",
volume = "39",
pages = "59--121",
journal = "SIAM Journal on Computing",
issn = "0097-5397",
publisher = "Society for Industrial and Applied Mathematics",
number = "1",

}

RIS

TY - JOUR

T1 - Narrow proofs may be spacious

T2 - Separating space and width in resolution

AU - Nordström, Jakob

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - Lower bound

KW - Pebble game

KW - Pebbling contradiction

KW - Proof complexity

KW - Resolution

KW - Separation

KW - Space

KW - Width

UR - http://www.scopus.com/inward/record.url?scp=67650162541&partnerID=8YFLogxK

U2 - 10.1137/060668250

DO - 10.1137/060668250

M3 - Journal article

AN - SCOPUS:67650162541

VL - 39

SP - 59

EP - 121

JO - SIAM Journal on Computing

JF - SIAM Journal on Computing

SN - 0097-5397

IS - 1

ER -

ID: 251871036