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.

Authors

• Marijn J. H. Heule
• Hans van Maaren

Keywords

No keywords are indexed for this paper.