FPGA-based hardware acceleration for Boolean satisfiability

ABSTRACT

We present an FPGA-based hardware solution to the Boolean satisfiability (SAT) problem, with the main goals of scalability and speedup. In our approach the traversal of the implication graph as well as conflict clause generation are performed in hardware, in parallel. The experimental results and their analysis, along with the performance models are discussed. We show that an order of magnitude improvement in runtime can be obtained over MiniSAT (the best-in-class software based approach) by using a Virtex-4 (XC4VFX140) FPGA device. The resulting system can handle instances with as many as 10K variables and 280K clauses.

REFERENCES

• 1: Miron Abramovici , Jose T. de Sousa , Daniel Saab, A massively-parallel easily-scalable satisfiability solver using reconfigurable hardware, Proceedings of the 36th ACM/IEEE conference on Design automation, p.684-690, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.310028]
• 2: Stephen A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing, p.151-158, May 03-05, 1971, Shaker Heights, Ohio, United States [doi>10.1145/800157.805047]
• 3: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 4: Gu, J., Purdom, P., Franco, J., and Wah, B. 1997. Algorithms for the satisfiability (SAT) problem: A survey. In Discrete Math. and Theoretical Computer Science, DIMACS, Rutgers, NJ, 19--151.
• 5: Gulati, K., Waghmode, M., Khatri, S., and Shi, W. 2008. Efficient, scalable hardware engine for Boolean satisfiability and unsatisfiable core extraction. IET Comput. Digit. Teclin. 2, 3, 214--229.
• 6: Oskar Mencer , Marco Platzner, Dynamic Circuit Generation for Boolean Satisfiability in an Object-Oriented Design Environment, Proceedings of the Thirty-Second Annual Hawaii International Conference on System Sciences-Volume 3, p.3044, January 05-08, 1999
• 7: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 8: Pagarani, T., Kocan, F., Saab, D., and Abraham, J. 2000. Parallel and scalable architecture for solving Satisfiability on reconfigurable FPGA. In Proceedings of the Custom Integrated Circuit Conference. 147--150.
• 9: Marco Platzner , Giovanni De Micheli, Acceleration of Satisfiability Algorithms by Reconfigurable Hardware, Proceedings of the 8th International Workshop on Field-Programmable Logic and Applications, From FPGAs to Computing Paradigm, p.69-78, August 31-September 03, 1998
• 10: M. Redekopp , Andreas Dandalis, A Parallel Pipelined SAT Solver for FPGAs, Proceedings of the The Roadmap to Reconfigurable Computing, 10th International Workshop on Field-Programmable Logic and Applications, p.462-468, August 27-30, 2000
• 11: Safar, M., El-Kharashi, M., and Salem, A. 2006. FPGA-based SAT solver. In Proceedings of the Canadian Conference on Electrical and Computer Engineering. 1901--1904.
• 12: Mona Safar , Mohamed Shalan , M. Watheq El-Kharashi , Ashraf Salem, Interactive presentation: A shift register based clause evaluator for reconfigurable SAT solver, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
• 13: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 14: Iouliia Skliarova , Antonio de Brito Ferrari, Reconfigurable Hardware SAT Solvers: A Survey of Systems, IEEE Transactions on Computers, v.53 n.11, p.1449-1461, November 2004 [doi>10.1109/TC.2004.102]
• 15: Iouliia Skliarova , António B. Ferrari, A software/reconfigurable hardware SAT solver, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.12 n.4, p.408-419, April 2004 [doi>10.1109/TVLSI.2004.825859]
• 16: Takayuki Suyama , Makoto Yokoo , Hiroshi Sawada , Akira Nagoya, Solving satisfiability problems using reconfigurable computing, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.9 n.1, p.109-117, Feb. 2001 [doi>10.1109/92.920826]
• 17: Matching Architecture to Application via Configurable Processors: A Case Study with Boolean Satisfiability Problem, Proceedings of the International Conference on Computer Design: VLSI in Computers & Processors, p.447, September 23-26, 2001
• 18: P. Zhong , M. Martonosi , P. Ashar , S. Malik, Accelerating Boolean Satisfiability with Configurable Hardware, Proceedings of the IEEE Symposium on FPGAs for Custom Computing Machines, p.186, April 15-17, 1998

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Algorithms implemented in hardware

General Terms:
Algorithms, Design, Performance

Keywords:
Boolean satisfiabilty (SAT), FPGA, boolean constant propagation (BCP), conflict induced clauses, non-chronological backtrack