Clause Form Conversions for Boolean Circuits

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.

• Type: Conference
• Year: 2004
• Where: SAT
• Authors: Paul Jackson, Daniel Sheridan
• Keywords: Boolean Circuits, Clause Form, Data Structure, SAT 2004