A practical reconfigurable hardware accelerator for Boolean satisfiability solvers

ABSTRACT

We present a practical FPGA-based accelerator for solving Boolean Satisfiability problems (SAT). Unlike previous efforts for hardware accelerated SAT solving, our design focuses on accelerating the most time consuming part of the SAT solver --- Boolean Constraint Propagation (BCP), leaving the choices of heuristics such as branching order, restarting policy, and learning and backtracking to software. Our novel approach uses an application-specific architecture instead of an instance-specific one to avoid time-consuming FPGA synthesis for each SAT instance. By avoiding global signal wires and carefully pipelining the design, our BCP accelerator is able to achieve much higher clock frequency than that of previous work. In addition, it can load SAT instances in milliseconds, can handle SAT instances with tens of thousands of variables and clauses using a single FPGA, and can easily scale to handle more clauses by using multiple FPGAs. Our evaluation on a cycle-accurate simulator shows that the FPGA co-processor can achieve 3.7--38.6x speedup on BCP compared to state-of-the-art software SAT solvers.

REFERENCES

• 1: Lintao Zhang , Sharad Malik, The Quest for Efficient Boolean Satisfiability Solvers, Proceedings of the 14th International Conference on Computer Aided Verification, p.17-36, July 27-31, 2002
• 2: 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]
• 3: P. Zhong, M. Martonosi, P. Ashar, and S. Malik, "Using Configurable Computing to Accelerate Boolean Satisfiability," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 18, no. 6, pp. 861--868, 1999
• 4: Peixin Zhong , Margaret Martonosi , Pranav Ashar , Sharad Malik, Solving Boolean Satisfiability with Dynamic Hardware Configurations, Proceedings of the 8th International Workshop on Field-Programmable Logic and Applications, From FPGAs to Computing Paradigm, p.326-335, August 31-September 03, 1998
• 5: 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
• 6: Miron Abramovici , Daniel G. Saab, Satisfiability on reconfigurable hardware, Proceedings of the 7th International Workshop on Field-Programmable Logic and Applications, p.448-456, September 01-03, 1997
• 7: 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]
• 8: 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]
• 9: Ying Zhao , Sharad Malik , Matthew Moskewicz , Conor Madigan, Accelerating boolean satisfiability through application specific processing, Proceedings of the 14th international symposium on Systems synthesis, September 30-October 03, 2001, Montréal, P.Q., Canada [doi>10.1145/500001.500059]
• 10: 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]
• 11: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 12: N. Een and A. Biere, "Effective Preprocessing in SAT through Variable and Clause Elimination," SAT 2005
• 13: Carla P. Gomes , Bart Selman , Henry Kautz, Boosting combinatorial search through randomization, Proceedings of the fifteenth national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, p.431-437, July 1998, Madison, Wisconsin, United States
• 14: J. Davis, Z. Tan, F. Yu, and L. Zhang, "Designing an Efficient Hardware Implication Accelerator for SAT Solving," SAT 2008
• 15: I. Kuon and J. Rose, "Measuring the Gap between FPGAs and ASICs," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 26, NO. 2, Feb. 2007, pp. 203--215.
• 16: "PCI Express Base 2.0 Specification,"http://www.pcisig.com/members/downloads/specifications/pciexpress/PCI_Express_Base_Rev_2.0_20Dec06a.pdf
• 17: Open FSB Initiative, Intel IDF, Spring 2007, Beijing
• 18: HyperTransport Technology I/O link, AMD, 2001
• 19: S. Kirkpatrick and B. Selman, "Critical Behavior in the Satisfiability of Random Boolean Formulae," Science, Vol. 264, pp. 1297--1301, May 27, 1994

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS

General Terms:
Design, Experimentation, Verification

Keywords:
BCP, FPGA, SAT solver, co-processor, reconfigurable