|
Informatics Report Series
|
|
|
|
|
|
|
|
|
| Title:Clause Form Conversions for Boolean Circuits |
| Authors:
Paul Jackson
; Daniel Sheridan
|
| Date:Aug 2005 |
| Publication Title:SAT 2004 (7th International Conference on Theory and Applications of Satisfiability Testing). Revised selected papers |
| Publisher:Springer |
|
Publication Type:Conference Paper
Publication Status:Published
|
|
Volume No:3542
Page Nos:183-198
|
|
DOI:10.1007/11527695_15
ISBN/ISSN:0302-9743
|
- Abstract:
-
The Boolean circuit is well established as a data structure for building propositional encodings of problems in preparation for sat- isfiability 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 pro- cedures on BMC problems demonstrating its superiority, and conclude that the CNF conversion has a significant role in reducing the overall solving time.
- Links To Paper
- 1st Link
- 2nd Link
- Bibtex format
- @InProceedings{EDI-INF-RR-0579,
- author = {
Paul Jackson
and Daniel Sheridan
},
- title = {Clause Form Conversions for Boolean Circuits},
- book title = {SAT 2004 (7th International Conference on Theory and Applications of Satisfiability Testing). Revised selected papers},
- publisher = {Springer},
- year = 2005,
- month = {Aug},
- volume = {3542},
- pages = {183-198},
- doi = {10.1007/11527695_15},
- url = {http://dx.doi.org/10.1007/11527695_15},
- }
|
