Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

Efficient Circuit to CNF Conversion

Panagiotis Manolios and Daron Vroon.
Theory and Applications of Satisfiability Testing (SAT-2007), 2007. © Springer-Verlag


Modern SAT solvers are proficient at solving Boolean satisfiability problems in Conjunctive Normal Form (CNF). However, these problems mostly arise from general Boolean circuits that are then translated to CNF. We outline a simple and expressive data structure for describing arbitrary circuits, as well as an algorithm for converting circuits to CNF. Our experimental results over a large benchmark suite show that the CNF problems we generate are consistently smaller and more quickly solved by modern SAT solvers than the CNF problems generated by current CNF generation methods.

PDF (229K) © Springer-Verlag