Marijn Heule, Matti Järvisalo, Armin Biere,
"Clause Elimination Procedures for CNF Formulas"
: 17th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science, Serie Lecture Notes in Computer Science (LNCS), Vol. 6397, Springer, Seite(n) 357?371, 2010
Original Titel:
Clause Elimination Procedures for CNF Formulas
Sprache des Titels:
Englisch
Original Buchtitel:
17th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science
Original Kurzfassung:
We develop and analyze clause elimination procedures, a specific family
of simplification techniques for conjunctive normal form (CNF) formulas. Extending
known procedures such as tautology, subsumption, and blocked clause
elimination, we introduce novel elimination procedures based on hidden and
asymmetric variants of these techniques.We analyze the resulting nine (including
five new) clause elimination procedures from various perspectives: size reduction,
BCP-preservance, confluence, and logical equivalence. For the variants not
preserving logical equivalence, we show how to reconstruct solutions to original
CNFs from satisfying assignments to simplified CNFs. We also identify a clause
elimination procedure that does a transitive reduction of the binary implication
graph underlying any CNF formula purely on the CNF level.