Clause Elimination Procedures for CNF Formulas

Abstract. 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.

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Marijn Heule, Matti Järvisalo, Armin Biere
• Keywords: Automated Reasoning, Clause Elimination, Clause Elimination Procedure, Logical Equivalence, LPAR 2010