NoteUnrestricted resolution versus N-resolution
Review articleOpen access
1992/02/03 Short communication DOI: 10.1016/0304-3975(92)90216-3
Journal: Theoretical Computer Science
AbstractAn N-resolution proof is a resolution proof in which the resolution rule is restricted: one clause to which it is applied must only consist of negative literals. N-resolution is complete (Schöning (1987), p. 109, Stickel (1985), p. 86). We construct an infinite family of propositional formulas and show: These formulas have unrestricted resolution proofs whose length is polynomially bounded in their size. All N-resolution proofs of these formulas are of superpolynomial length.
Request full text