Article ID Journal Published Year Pages File Type
6874144 Information Processing Letters 2018 7 Pages PDF
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.
Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
,