Aligning CNF- and Equivalence-Reasoning

Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translating to CNF. The best known example of this feature is probably provided by the parity-family. The larger such CNF formulas cannot be solved in reasonable time if no extra reasoning with - and detection of - these clauses is incorporated. That is, in solving these formulas, there is a more or less separated algorithmic device in dealing with these equivalence clauses, called equivalence reasoning, and another dealing with the remaining clauses. In this paper we propose a way to align these two reasoning devices by introducing parameters for which we establish optimal settings over a variety of existing benchmarks. We obtain a truly convincing speed up in solving such formulas with respect to the best solving methods existing so far.

• Type: Conference
• Year: 2004
• Where: SAT
• Authors: Marijn Heule, Hans van Maaren
• Keywords: CNF Formulas, Equivalence Clauses, SAT 2004, Structural Logical Formulas