Informatics Report Series


Report   

EDI-INF-RR-0579


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Clause Form Conversions for Boolean Circuits
Authors: Paul Jackson ; Daniel Helson ; 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 Helson 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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh