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.

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Stefan Szeider
• Keywords: Automated Reasoning, CADE 2001, Read-once Resolution