
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Iouliia Skliarova, António de Brito Ferrari, "Reconfigurable Hardware SAT Solvers: A Survey of Systems," IEEE Transactions on Computers, vol. 53, no. 11, pp. 14491461, November, 2004.  
BibTex  x  
@article{ 10.1109/TC.2004.102, author = {Iouliia Skliarova and António de Brito Ferrari}, title = {Reconfigurable Hardware SAT Solvers: A Survey of Systems}, journal ={IEEE Transactions on Computers}, volume = {53}, number = {11}, issn = {00189340}, year = {2004}, pages = {14491461}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2004.102}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Reconfigurable Hardware SAT Solvers: A Survey of Systems IS  11 SN  00189340 SP1449 EP1461 EPD  14491461 A1  Iouliia Skliarova, A1  António de Brito Ferrari, PY  2004 KW  Boolean satisfiability KW  reconfigurable computing KW  FPGA KW  hardware acceleration. VL  53 JA  IEEE Transactions on Computers ER   
[1] G. Estrin, Reconfigurable Computer Origins: The UCLA FixedPlusVariable (F+V) Structure Computer IEEE Annals of the History of Computing, pp. 39, Oct./Dec. 2002.
[2] S.A. Guccione, Reconfigurable Computing at Xilinx keynote talk, EUROMICRO Symp. Digital System Design, Sept. 2001.
[3] W.H. MangioneSmith and B.L. Hutchings, Configurable Computing: The Road Ahead Proc. Reconfigurable Architectures Workshop, pp. 8196, 1997.
[4] R. Tessier and W. Burleson, Reconfigurable Computing for Digital Signal Processing: A Survey J. VLSI Signal Processing, vol. 28, nos. 12, pp. 727, 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. 19151, 1997.
[6] S.A. Cook, The Complexity of TheoremProving Procedures Proc. Third ACM Symp. Theory of Computing, pp. 151158, 1971.
[7] M. Davis, G. Logemann, and D. Loveland, A Machine Program for Theorem Proving Comm. ACM, no. 5, pp. 394397, 1962.
[8] P. Goel, An Implicit Enumeration Algorithm to Generate Tests for Combinatorial Logic Circuits IEEE Trans. Computers, vol. 30, no. 3, pp. 215222, 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. 506521, 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. 440446, July 1992.
[12] B. Selman, H. Kautz, and B. Cohen, Noise Strategies for Improving Local Search Proc. 12th Nat'l Conf. Artificial Intelligence, pp. 337343, 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. 497509, 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. 109116, 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. 179186, 1998.
[17] P. Zhong, M. Martonosi, P. Ashar, and S. Malik, Using Configurable Computing to Accelerate Boolean Satisfiability IEEE Trans. ComputerAided Design of Integrated Circuits and Systems, vol. 18, no. 6, pp. 861868, 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. 194199, 1998.
[19] P. Zhong, M. Martonosi, P. Ashar, and S. Malik, Solving Boolean Satisfiability with Dynamic Hardware Configurations FieldProgrammable Logic: From FPGAs to Computing Paradigm, R.W. Hartenstein and A. Keevallik, eds., pp. 326235, 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 ObjectOriented Design Environment Proc. 32nd Hawaii Int'l Conf. System Sciences (HICSS32 (ConfigwareReconfigurable Eng. track), 1999.
[22] M. Platzner and G. De Micheli, Acceleration of Satisfiability Algorithms by Reconfigurable Hardware FieldProgrammable Logic: From FPGAs to Computing Paradigm, R.W. Hartenstein and A. Keevallik, eds., pp. 6978, Springer, 1998.
[23] M. Abramovici and D. Saab, Satisfiability on Reconfigurable Hardware Proc. Seventh Int'l Workshop FieldProgrammable Logic and Applications, pp. 448456, 1997.
[24] M. Abramovici and J.T. de Sousa, A SAT Solver Using Reconfigurable Hardware and Virtual Logic J. Automated Reasoning, vol. 24, nos. 12, pp. 536, 2000.
[25] A. Dandalis and V.K. Prasanna, RunTime Performance Optimization of an FPGABased Deduction Engine for SAT Solvers ACM Trans. Design Automation of Electronic Systems, vol. 7, no. 4, pp. 547562, Oct. 2002.
[26] M. Redekopp and A. Dandalis, A Parallel Pipelined SAT Solver for FPGA's Proc. 10th Int'l Conf. FieldProgrammable Logic and Applications, pp. 462468, 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. 352357, 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. 526531, 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. 197201, 2001.
[30] J. de Sousa, J.P. MarquesSilva, and M. Abramovici, A Configware/Software Approach to SAT Solving Proc. Ninth IEEE Int'l Symp. FieldProgrammable 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. FieldProgrammable Custom Computing Machines, pp. 282283, 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. 498503, 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. 408419, 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. 270277, 2002.
[35] R.H.C. Yap, S.Z.Q. Wang, and M.J. Henz, Hardware Implementations of RealTime Reconfigurable WSAT Variants Proc. 13th Int'l Conf. FieldProgrammable Logic and Applications, pp. 488496, 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. 209215, 1997.
[37] A. Rashid, J. Leonard, and W.H. MangioneSmith, Dynamic Circuit Generation for Solving Specific Problem Instances of Boolean Satisfiability Proc. Sixth IEEE Symp. FPGAs for Custom Computing Machines, pp. 196205, 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. FieldProgrammable 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.tudarmstadt.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. 530535, 2001.
[44] E. Goldberg and Y. Novikov, BerkMin: A Fast and Robust SATSolver Proc. Design, Automation and Test in Europe Conf., pp. 142149, 2002.