NP-Completeness of Refutability by
in Automated Reasoning - Proceedings of the First
International Joint Conference on Automated Reasoning (IJCAR 2001) Siena,
Italy, June 2001; Eds.: R. Goré, A. Leitsch and T. Nipkow; Lecture
Notes in Artificial Intelligence 2083, pp.168-181, Springer Verlag,
Download:   [paper ps]
A boolean formula in conjunctive normal form (CNF) F is refuted
by literal-once resolution if the empty clause is
inferred from F by resolving on each literal of F at most
once. Literal-once resolution refutations can be found
nondeterministically in polynomial time, though this restricted
system is not complete.
We show that despite of the weakness of
literal-once resolution, the recognition of CNF-formulas which
are refutable by literal-once resolution is NP-complete.
We study the relationship between literal-once resolution and
read-once resolution (introduced by Iwama and Miyano).
Further we answer a question posed by Kullmann related to minimal
[back to Stefan