NP-Completeness of Refutability by
Literal-Once Resolution
Stefan Szeider
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,
2001.
Download: [paper ps]
[paper pdf]
Abstract:
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
unsatisfiability.
[back to Stefan
Szeider's homepage]
|