FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers
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.
KeywordsHost Computer Conflict Detector Reconfigurable Computing Implication Graph Binary Clause
- 4.Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. on Computers C-35(8) (August 1986)Google Scholar
- 5.Marques-Silva, J.P., Guerra e Silva, L.: Solving Satisfiability in Combinational Circuits. IEEE Design and Test of Computers, 16–21 (July/August 2003)Google Scholar
- 6.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)Google Scholar