Sciweavers

SAT
2004
Springer

The Optimality of a Fast CNF Conversion and its Use with SAT

13 years 9 months ago
The Optimality of a Fast CNF Conversion and its Use with SAT
Despite the widespread use and study of Boolean satisfiability for a diverse range of problem domains, encoding of problems is usually given to general propositional logic with little or no discussion of the conversion to clause form that will be necessary. In this paper we present a fast and easy to implement conversion to equisatisfiable clause form for Boolean circuits. Since the conversion is equivalent to that of Boy de la Tour it is optimal in the number of clauses produced. We present experimental results comparing this and other conversion procedures on BMC problems and conclude that the CNF conversion plays a large part in reducing the overall solving time.
Daniel Sheridan
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where SAT
Authors Daniel Sheridan
Comments (0)