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

Forskningsoutput: TidskriftsbidragArtikel i vetenskaplig tidskriftPeer review

Sammanfattning

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.

Originalspråkengelska
Sidor (från-till)59-121
Antal sidor63
TidskriftSIAM Journal on Computing
Volym39
Nummer1
DOI
StatusPublished - 2009
Externt publiceradJa

Ämnesklassifikation (UKÄ)

  • Datavetenskap (datalogi)

Fingeravtryck

Utforska forskningsämnen för ”Narrow proofs may be spacious: Separating space and width in resolution”. Tillsammans bildar de ett unikt fingeravtryck.

Citera det här