zbMATH — the first resource for mathematics

Clause form conversions for Boolean circuits. (English) Zbl 1122.68603
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, 183-198 (2005).
Summary: The Boolean circuits is well established as a data structure for building propositional encodings of problems in preparation for satisfiability solving. The standard method for converting Boolean circuits to clause form (naming every vertex) has a number of shortcomings.
In this paper we give a projection of several well-known clause form conversions to a simplified form of Boolean circuit. We introduce a new conversion which we show is equivalent to that of Boy de la Tour in certain circumstances and is hence optimal in the number of clauses that it produces. We extend the algorithm to cover reduced Boolean circuits, a data structure used by the model checker NuSMV.
We present experimental results for this and other conversion procedures on BMC problems demonstrating its superiority, and conclude that the CNF conversion has a significant role in reducing the overall solving time.
For the entire collection see [Zbl 1075.68002].

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