This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Reconfigurable Hardware SAT Solvers: A Survey of Systems
November 2004 (vol. 53 no. 11)
pp. 1449-1461
By adapting to computations that are not so well-supported by general-purpose processors, reconfigurable systems achieve significant increases in performance. Such computational systems use high-capacity programmable logic devices and are based on processing units customized to the requirements of a particular application. A great deal of the research effort in this area is aimed at accelerating the solution of combinatorial optimization problems. Special attention in this context was given to the Boolean satisfiability (SAT) problem resulting in a considerable number of different architectures being proposed. This paper presents the state-of-the-art in reconfigurable hardware SAT satisfiers. The analysis and classification of existing systems has been performed according to such criteria as algorithmic issues, reconfiguration modes, the execution model, the programming model, logic capacity, and performance.

[1] G. Estrin, Reconfigurable Computer Origins: The UCLA Fixed-Plus-Variable (F+V) Structure Computer IEEE Annals of the History of Computing, pp. 3-9, Oct./Dec. 2002.
[2] S.A. Guccione, Reconfigurable Computing at Xilinx keynote talk, EUROMICRO Symp. Digital System Design, Sept. 2001.
[3] W.H. Mangione-Smith and B.L. Hutchings, Configurable Computing: The Road Ahead Proc. Reconfigurable Architectures Workshop, pp. 81-96, 1997.
[4] R. Tessier and W. Burleson, Reconfigurable Computing for Digital Signal Processing: A Survey J. VLSI Signal Processing, vol. 28, nos. 1-2, pp. 7-27, 2001.
[5] J. Gu, P.W. Purdom, J. Franco, and B.W. Wah, Algorithms for the Satisfiability (SAT) Problem: A Survey DIMACS Series in Discrete Math. and Theoretical Computer Science, vol. 35, pp. 19-151, 1997.
[6] S.A. Cook, The Complexity of Theorem-Proving Procedures Proc. Third ACM Symp. Theory of Computing, pp. 151-158, 1971.
[7] M. Davis, G. Logemann, and D. Loveland, A Machine Program for Theorem Proving Comm. ACM, no. 5, pp. 394-397, 1962.
[8] P. Goel, An Implicit Enumeration Algorithm to Generate Tests for Combinatorial Logic Circuits IEEE Trans. Computers, vol. 30, no. 3, pp. 215-222, Mar. 1981.
[9] L.M. Silva and K.A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability IEEE Trans. Computers, vol. 48, no. 5, pp. 506-521, May 1999.
[10] Z. Michalewicz and D.B. Fogel, How to Solve It: Modern Heuristics. Springer, 2000.
[11] B. Selman, H. Levesque, and D. Mitchell, A New Method for Solving Hard Satisfiability Problems Proc. Nat'l Conf. Am. Assoc. Artificial Intelligence (AAAI'92), pp. 440-446, July 1992.
[12] B. Selman, H. Kautz, and B. Cohen, Noise Strategies for Improving Local Search Proc. 12th Nat'l Conf. Artificial Intelligence, pp. 337-343, July 1994.
[13] M. Yokoo, T. Suyama, and H. Sawada, Solving Satisfiability Problems Using Field Programmable Gate Arrays: First Results Proc. Second Int'l Conf. Principles and Practice of Constraint Programming, pp. 497-509, 1996.
[14] T. Suyama, M. Yokoo, H. Sawada, and A. Nagoya, Solving Satisfiability Problems Using Reconfigurable Computing IEEE Trans. VLSI Systems, vol. 9, no. 1, pp. 109-116, 2001.
[15] T. Suyama, M. Yokoo, and A. Nagoya, Solving Satisfiability Problems on FPGAs Using Experimental Unit Propagation Proc. Fifth Int'l Conf. Principles and Practice of Constraint Programming, 1999.
[16] T. Suyama, M. Yokoo, and H. Sawada, Solving Satisfiability Problems Using Logic Synthesis and Reconfigurable Hardware Proc. 31st Hawaii Int'l Conf. System Sciences, vol. 7, pp. 179-186, 1998.
[17] 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.
[18] P. Zhong, P. Ashar, S. Malik, and M. Martonosi, Using Reconfigurable Computing Techniques to Accelerate Problems in the CAD Domain: A Case Study with Boolean Satisfiability Proc. Design Automation Conf., pp. 194-199, 1998.
[19] P. Zhong, M. Martonosi, P. Ashar, and S. Malik, Solving Boolean Satisfiability with Dynamic Hardware Configurations Field-Programmable Logic: From FPGAs to Computing Paradigm, R.W. Hartenstein and A. Keevallik, eds., pp. 326-235, Springer, 1998.
[20] P. Zhong, Using Configurable Computing to Accelerate Boolean Satisfiability PhD dissertation, Dept. of Electrical Eng., Princeton Univ., 1999.
[21] O. Mencer and M. Platzner, Dynamic Circuit Generation for Boolean Satisfiability in an Object-Oriented Design Environment Proc. 32nd Hawaii Int'l Conf. System Sciences (HICSS-32 (Configware-Reconfigurable Eng. track), 1999.
[22] M. Platzner and G. De Micheli, Acceleration of Satisfiability Algorithms by Reconfigurable Hardware Field-Programmable Logic: From FPGAs to Computing Paradigm, R.W. Hartenstein and A. Keevallik, eds., pp. 69-78, Springer, 1998.
[23] M. Abramovici and D. Saab, Satisfiability on Reconfigurable Hardware Proc. Seventh Int'l Workshop Field-Programmable Logic and Applications, pp. 448-456, 1997.
[24] M. Abramovici and J.T. de Sousa, A SAT Solver Using Reconfigurable Hardware and Virtual Logic J. Automated Reasoning, vol. 24, nos. 1-2, pp. 5-36, 2000.
[25] A. Dandalis and V.K. Prasanna, Run-Time Performance Optimization of an FPGA-Based Deduction Engine for SAT Solvers ACM Trans. Design Automation of Electronic Systems, vol. 7, no. 4, pp. 547-562, Oct. 2002.
[26] M. Redekopp and A. Dandalis, A Parallel Pipelined SAT Solver for FPGA's Proc. 10th Int'l Conf. Field-Programmable Logic and Applications, pp. 462-468, 2000.
[27] C.K. Chung and P.H.W. Leong, An Architecture for Solving Boolean Satisfiability Using Runtime Configurable Hardware Proc. Int'l Workshop Parallel Processing, pp. 352-357, 1999.
[28] W.H. Yung, Y.W. Seung, K.H. Lee, and P.H.W. Leong, A Runtime Reconfigurable Implementation of the GSAT Algorithm Proc. Ninth Int'l Workshop Field Programmable Logic and Applications, pp. 526-531, 1999.
[29] P.H.W. Leong, C.W. Sham, W.C. Wong, H.Y. Wong, W.S. Yuen, and M.P. Leong, A Bitstream Reconfigurable FPGA Implementation of the WSAT Algorithm IEEE Trans. VLSI Systems, vol. 9, no. 1, pp. 197-201, 2001.
[30] J. de Sousa, J.P. Marques-Silva, and M. Abramovici, A Configware/Software Approach to SAT Solving Proc. Ninth IEEE Int'l Symp. Field-Programmable Custom Computing Machines, 2001.
[31] N.A. Reis and J.T. de Sousa, On Implementing a Configware/Software SAT Solver Proc. 10th IEEE Int'l Symp. Field-Programmable Custom Computing Machines, pp. 282-283, 2002.
[32] R.C. Ripado and J.T. de Sousa, A Simulation Tool for a Pipelined SAT Solver Proc. XVI Conf. Design of Circuits and Integrated Systems, pp. 498-503, Nov. 2001.
[33] I. Skliarova and A.B. Ferrari, A Software/Reconfigurable Hardware SAT Solver IEEE Trans. Very Large Scale Integration (VLSI) Systems, vol. 12, no. 4, pp. 408-419, Apr. 2004.
[34] I. Skliarova and A.B. Ferrari, A Hardware/Software Approach to Accelerate Boolean Satisfiability Proc. IEEE Design and Diagnostics of Electronic Circuits and Systems Workshop, pp. 270-277, 2002.
[35] R.H.C. Yap, S.Z.Q. Wang, and M.J. Henz, Hardware Implementations of Real-Time Reconfigurable WSAT Variants Proc. 13th Int'l Conf. Field-Programmable Logic and Applications, pp. 488-496, 2003.
[36] Y. Hamadi and D. Merceron, Reconfigurable Architectures: A New Vision for Optimization Problems Proc. Third Int'l Conf. Principles and Practice of Constraint Programming, pp. 209-215, 1997.
[37] A. Rashid, J. Leonard, and W.H. Mangione-Smith, Dynamic Circuit Generation for Solving Specific Problem Instances of Boolean Satisfiability Proc. Sixth IEEE Symp. FPGAs for Custom Computing Machines, pp. 196-205, 1998.
[38] M. Boyd and T. Larrabee, ELVIS a Scalable, Loadable Custom Programmable Logic Device for Solving Boolean Satisfiability Problems Proc. Eight IEEE Int'l Symp. Field-Programmable Custom Computing Machines, 2000.
[39] J.W. Freeman, Improvements to Propositional Satisfiability Search Algorithms PhD dissertation, Univ. of Pennsylvania, 1995.
[40] DIMACS challenge benchmarks,http://www.intellektik.informa tik.tu-darmstadt.de/ SATLIBbenchm.html, 2001.
[41] L. Simon, D. Le Berre, and E. Hirsch, The SAT2002 Competition. Technical Report (preliminary draft) http://www.satlive.org/SATCompetition onlinereport.pdf , 2002.
[42] 2003 SAT Competition,http://www.lri.fr/~simon/contest03results /, 2003.
[43] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: Engineering an Efficient SAT Solver Proc. 38th Design Automation Conf., pp. 530-535, 2001.
[44] E. Goldberg and Y. Novikov, BerkMin: A Fast and Robust SAT-Solver Proc. Design, Automation and Test in Europe Conf., pp. 142-149, 2002.

Index Terms:
Boolean satisfiability, reconfigurable computing, FPGA, hardware acceleration.
Citation:
Iouliia Skliarova, António de Brito Ferrari, "Reconfigurable Hardware SAT Solvers: A Survey of Systems," IEEE Transactions on Computers, vol. 53, no. 11, pp. 1449-1461, Nov. 2004, doi:10.1109/TC.2004.102
Usage of this product signifies your acceptance of the Terms of Use.