zbMATH — the first resource for mathematics

Aligning CNF- and equivalence-reasoning. (English) Zbl 1122.68600
Hoos, Holger H. (ed.) et al., Theory and applications of satisfiability testing. 7th international conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-27829-X/pbk). Lecture Notes in Computer Science 3542, 145-156 (2005).
Summary: Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translation to CNF. Probably the best known example of this is the parity-family. Large instances of such CNF formulas cannot be solved in reasonable time if no detection of, and extra reasoning with, these clauses is incorporated. That is, in solving these formulas, there is a more or less separate algorithmic device dealing with the 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 values 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.
For the entire collection see [Zbl 1075.68002].

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI