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

Forskningsoutput: Kapitel i bok/rapport/Conference proceedingKonferenspaper i proceeding

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

Detaljer

Författare
Externa organisationer
  • KTH Royal Institute of Technology
Forskningsområden

Ämnesklassifikation (UKÄ) – OBLIGATORISK

  • Datavetenskap (datalogi)

Nyckelord

Originalspråkengelska
Titel på värdpublikationSTOC'06
Undertitel på gästpublikationProceedings of the 38th Annual ACM Symposium on Theory of Computing
FörlagAssociation for Computing Machinery (ACM)
Sidor507-516
Antal sidor10
ISBN (tryckt)1595931341, 9781595931344
StatusPublished - 2006
PublikationskategoriForskning
Peer review utfördJa
Externt publiceradJa
Evenemang38th Annual ACM Symposium on Theory of Computing, STOC'06 - Seattle, WA, USA
Varaktighet: 2006 maj 212006 maj 23

Publikationsserier

NamnProceedings of the Annual ACM Symposium on Theory of Computing
FörlagACM
Volym2006
ISSN (tryckt)0737-8017

Konferens

Konferens38th Annual ACM Symposium on Theory of Computing, STOC'06
LandUSA
OrtSeattle, WA
Period2006/05/212006/05/23