Sciweavers

CADE
2001
Springer

NP-Completeness of Refutability by Literal-Once Resolution

14 years 11 months ago
NP-Completeness of Refutability by Literal-Once Resolution
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.
Stefan Szeider
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2001
Where CADE
Authors Stefan Szeider
Comments (0)