Abstract
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 research effort in this area is aimed at accelerating the solution of combinatorial optimization problems. Special attention 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 of existing systems has been performed according to such criteria as reconfiguration modes, the execution model, the programming model, etc.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Estrin, G.: Reconfigurable Computer Origins: The UCLA Fixed-Plus-Variable (F+V) Structure Computer. IEEE Annals of the History of Computing, 3–9 (October-December 2002)
Gu, J., Purdom, P.W., Franco, J., Wah, B.W.: Algorithms for the Satisfiability (SAT) Problem: A Survey. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35, pp. 19–151 (1997)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NPCompleteness. W.H. Freeman and Company, San Francisco (1979)
Yokoo, M., Suyama, T., Sawada, H.: Solving Satisfiability Problems Using Field Programmable Gate Arrays: First Results. In: Proc. of 2nd Int. Conf. on Principles and Practice of Constraint Programming, pp. 497–509 (1996)
Suyama, T., Yokoo, M., Sawada, H., Nagoya, A.: Solving Satisfiability Problems Using Reconfigurable Computing. IEEE Trans. on VLSI Systems 9(1), 109–116 (2001)
Freeman, J.W.: Improvements to Propositional Satisfiability Search Algorithms. Ph.D. dissertation. Univ. Pennsylvania (1995)
DIMACS challenge benchmarks [online], Available: http://www.intellektik.informatik.tudarmstadt.de/SATLIB/bencm.html
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM (5), 394–397 (1962)
Zhong, P., Martonosi, M., Ashar, P., Malik, S.: Using Configurable Computing to Accelerate Boolean Satisfiability. IEEE Trans. CAD of Integrated Circuits and Systems 18(6), 861–868 (1999)
Zhong, P., Ashar, P., Malik, S., Martonosi, M.: Using reconfigurable computing techniques to accelerate problems in the CAD domain: a case study with Boolean satisfiability. In: Proc. Design Automation Conf., pp. 194–199 (1998)
Zhong, P., Martonosi, M., Ashar, P., Malik, S.: Solving Boolean satisfiability with dynamic hardware configurations. In: Hartenstein, R.W., Keevallik, A. (eds.) FPL 1998. LNCS, vol. 1482, pp. 326–335. Springer, Heidelberg (1998)
Zhong, P.: Using Configurable Computing to Accelerate Boolean Satisfiability. Ph.D. dissertation. Department of Electrical Engineering. Princeton University (1999)
Silva, L.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Computers, vol. 48(5), 506–521 (1999)
Abramovici, M., Saab, D.: Satisfiability on Reconfigurable Hardware. In: Proc. 7th Int. Workshop on Field-Programmable Logic and Applications, pp. 448–456 (1997)
Abramovici, M., de Sousa, J.T.: A SAT solver using reconfigurable hardware and virtual logic. Journal of Automated Reasoning 24(1-2), 5–36 (2000)
Platzner, M.: Reconfigurable accelerators for combinatorial problems. IEEE Computer, 58–60 (April 2000)
Platzner, M., De Micheli, G.: Acceleration of satisfiability algorithms by reconfigurable hardware. In: Hartenstein, R.W., Keevallik, A. (eds.) FPL 1998. LNCS, vol. 1482, pp. 69–78. Springer, Heidelberg (1998)
Boyd, M., Larrabee, T.: ELVIS – a scalable, loadable custom programmable logic device for solving Boolean satisfiability problems. In: Proc. 8th IEEE Int. Symp. on Field-Programmable Custom Computing Machines - FCCM (2000)
de Sousa, J., Marques-Silva, J.P., Abramovici, M.: A configware/software approach to SAT solving. In: Proc. of 9th IEEE Int. Symp. on Field-Programmable Custom Computing Machines (2001)
Reis, N.A., de Sousa, J.T.: On Implementing a Configware/Software SAT Solver. In: Proc. of 10th IEEE Int. Symp. Field-Programmable Custom Computing Machines, pp. 282–283 (2002)
Skliarova, I., Ferrari, A.B.: A SAT Solver Using Software and Reconfigurable Hardware. In: Proc. of the Design, Automation and Test in Europe Conference, p. 1094 (2002)
Skliarova, I., Ferrari, A.B.: A hardware/software approach to accelerate Boolean satisfiability. In: Proc. of IEEE Design and Diagnostics of Electronic Circuits and Systems Workshop, pp. 270–277 (2002)
Simon, L., Le Berre, D., Hirsch, E.: The SAT 2002 Competition. Technical Report (2002) (preliminary draft) [Online]. Available: http://www.satlive.org/SATCompetition/onlinereport.pdf
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. of the 38th Design Automation Conference, pp. 530–535 (2001)
Goldberg, E., Novikov, Y.: BerkMin: a Fast and Robust SAT-solver. In: Proc. Design, Automation and Test in Europe Conference, pp.142–149 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Skliarova, I., Ferrari, A.B. (2003). Reconfigurable Hardware SAT Solvers: A Survey of Systems. In: Y. K. Cheung, P., Constantinides, G.A. (eds) Field Programmable Logic and Application. FPL 2003. Lecture Notes in Computer Science, vol 2778. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45234-8_46
Download citation
DOI: https://doi.org/10.1007/978-3-540-45234-8_46
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40822-2
Online ISBN: 978-3-540-45234-8
eBook Packages: Springer Book Archive