Advertisement
Published in:
2010 | OriginalPaper | Chapter
Clause Elimination Procedures for CNF Formulas
Authors : Marijn Heule, Matti Järvisalo, Armin Biere
Published in: Logic for Programming, Artificial Intelligence, and Reasoning
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.