In this note we show two results about k-DNF resolution. First we prove that there are CNF formulas which require exponential length refutations in resolution extended with parities of size k, but have polynomial length refutations in k-DNF resolution. Then we show that small proofs in tree-like k-DNF resolution and narrow proofs in dag-like resolution have the same proving power, over CNFs. This latter result is clearly implicit in Krajíček (1994) [24] but this direct proof is focused on resolution and provides information about refutation width.
A note about k-DNF resolution / Lauria, Massimo. - In: INFORMATION PROCESSING LETTERS. - ISSN 0020-0190. - 137:(2018), pp. 33-39. [10.1016/j.ipl.2018.04.014]
A note about k-DNF resolution
Lauria, Massimo
2018
Abstract
In this note we show two results about k-DNF resolution. First we prove that there are CNF formulas which require exponential length refutations in resolution extended with parities of size k, but have polynomial length refutations in k-DNF resolution. Then we show that small proofs in tree-like k-DNF resolution and narrow proofs in dag-like resolution have the same proving power, over CNFs. This latter result is clearly implicit in Krajíček (1994) [24] but this direct proof is focused on resolution and provides information about refutation width.| File | Dimensione | Formato | |
|---|---|---|---|
|
Lauria_k-DNF-resolution_2018.pdf
solo gestori archivio
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
336.35 kB
Formato
Adobe PDF
|
336.35 kB | Adobe PDF | Contatta l'autore |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
