Abstract
We present an FPGA-based accelerator for 3-SAT clause evaluation and conflict diagnosis and propose an approach to incorporate it in solving the Combinational Equivalence Checking problem. SAT binary clauses are mapped onto an implication graph and the ternary clauses are kept in an indexed clause database and mapped into the clause evaluator and conflict analyzer on FPGA.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Compton, K., Hauck, S.: Reconfigurable Computing: A Survey of Systems and Software. ACM computing Surveys 34(2), 171–210 (2002)
Skliarova, I., Ferrari, A.B.: Reconfigurable Hardware SAT Solvers: A Survey of Systems. IEEE Transactions on Computers 53(11), 1449–1461 (2004)
Silva, L.M., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. Computers 48(5), 506–521 (1999)
Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. on Computers C-35(8) (August 1986)
Marques-Silva, J.P., Guerra e Silva, L.: Solving Satisfiability in Combinational Circuits. IEEE Design and Test of Computers, 16–21 (July/August 2003)
Reda, S., Salem, A.: Combinational Equivalence Checking using Boolean Satisfiability and Binary Decision Diagrams. IEEE/ACM Design, Automation and Test in Europe, 122–126 (March 2001)
Zhong, P., Martonosi, M., Ashar, P., Malik, S.: Using Configurable Computing to Accelerate Boolean Satisfiability. IEEE Trans. Computer Aided Design of Integrated Circuits and Systems 18(6), 861–868 (1999)
Larrabee, T.: Test Pattern generation using Boolean Satisfiability. IEEE Transactions on 2Computer Aided Design 11(1), 4–15 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Safar, M., El-Kharashi, M.W., Salem, A. (2005). FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers. In: Borrione, D., Paul, W. (eds) Correct Hardware Design and Verification Methods. CHARME 2005. Lecture Notes in Computer Science, vol 3725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560548_37
Download citation
DOI: https://doi.org/10.1007/11560548_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29105-3
Online ISBN: 978-3-540-32030-2
eBook Packages: Computer ScienceComputer Science (R0)