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
APA
Vancouver
Author
Bibtex
}
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