FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers

  • Mona Safar
  • M. Watheq El-Kharashi
  • Ashraf Salem
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


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.


Host Computer Conflict Detector Reconfigurable Computing Implication Graph Binary Clause 
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.


  1. 1.
    Compton, K., Hauck, S.: Reconfigurable Computing: A Survey of Systems and Software. ACM computing Surveys 34(2), 171–210 (2002)CrossRefGoogle Scholar
  2. 2.
    Skliarova, I., Ferrari, A.B.: Reconfigurable Hardware SAT Solvers: A Survey of Systems. IEEE Transactions on Computers 53(11), 1449–1461 (2004)CrossRefGoogle Scholar
  3. 3.
    Silva, L.M., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. Computers 48(5), 506–521 (1999)CrossRefGoogle Scholar
  4. 4.
    Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. on Computers C-35(8) (August 1986)Google Scholar
  5. 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. 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
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Larrabee, T.: Test Pattern generation using Boolean Satisfiability. IEEE Transactions on 2Computer Aided Design 11(1), 4–15 (1992)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Mona Safar
    • 1
  • M. Watheq El-Kharashi
    • 2
  • Ashraf Salem
    • 3
  1. 1.Computer and Systems DepartmentAin Shams UniversityCairoEgypt
  2. 2.University of VictoriaVictoriaCanada
  3. 3.Mentor Graphics EgyptCairoEgypt

Personalised recommendations