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