Abstract
This paper proposes an architecture that combines a context-switching virtual configware/software SAT solver with an embedded processor to promote a tighter coupling between configware and software. The virtual circuit is an arbitrarily large clause pipeline, partitioned into sections of a number of stages (hardware pages), which can fit in the configware. The hardware performs logical implications, grades and select decision variables. The software monitors the data and takes care of the high-level algorithmic flow. Experimental results show speed-ups that reach up to two orders of magnitude in one case. Future improvements for addressing scalability and performance issues are also discussed.
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
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)
RC1000 configware platform, http://www.celoxica.com
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP Completeness. W.H. Freeman and Company, San Francisco (1979)
Silva, J.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Computers 48(5), 506–521 (1999)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. 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)
DIMACS challenge benchmarks, http://www.intellektik.informatik.tudarmstadt.de/SATLIB/benchm.html
Suyama, T., Yokoo, M., Sawada, H., Nagoya, A.: Solving Satisfiability Problems Using Reconfigurable Computing. IEEE Trans. on VLSI Systems 9(1), 109–116 (2001)
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)
Platzner, M.: Reconfigurable accelerators for combinatorial problems. IEEE Computer, pp. 580–560 (April 2000)
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)
Dandalis, Prasanna, V.K.: Run-time performance optimization of an FPGA-based deduction engine for SAT solvers. ACM Trans. on Design Automation of Electronic Systems 7(4), 547–562 (2002)
Leong, P.H.W., Sham, C.W., Wong, W.C., Wong, H.Y., Yuen, W.S., Leong, M.P.: A Bitstream Reconfigurable FPGA Implementation of the WSAT algorithm. IEEE Trans. On VLSI Systems 9(1), 197–201 (2001)
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 (2000)
de Sousa, J., Marques-Silva, J.P., Abramovici, M.: A configware/software approach to SAT solving. In: Proc. 9th IEEE Int. Symp. on Field-Programmable Custom Computing Machines (2001)
Skliarova, Ferrari, A.B.: A SAT Solver Using Software and Reconfigurable Hardware. In: Proc. the Design, Automation and Test in Europe Conference 2002, p. 1094 (2002)
Davis, M., Putnam, H.: A Computing Procedure for Quantication Theory. ACM journal 7, 201–215 (1960)
Yap, R.H.C., Wang, S.Z.Q., Henz, M.J.: Hardware Implementations of Real-Time Reconfigurable WSAT Variants. In: Y. K. Cheung, P., Constantinides, G.A. (eds.) FPL 2003. LNCS, vol. 2778, pp. 488–496. Springer, Heidelberg (2003)
Skliarova, Ferrari, A.B.: In: Y. K. Cheung, P., Constantinides, G.A. (eds.) FPL 2003. LNCS, vol. 2778, pp. 468–477. Springer, Heidelberg (2003)
MicroBlaze Soft Processor, http://www.xilinx.com/xlnx/xil_prodcat_product.jsp?title=microblaze
Reis, N.A., de Sousa, J.T.: On Implementing a Configware/Software SAT Solver. In: Proc. 10th IEEE Int. Symp. Field-Programmable Custom Computing Machines, pp. 282–283 (2002)
Ripado, R.C., de Sousa, J.T.: A Simulation Tool for a Pipelined SAT Solver. In: Proc. XVI Conf. on Design of Circuits and Integrated Systems, November 2001, pp. 498–503 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tavares, C.J., Bungardean, C., Matos, G.M., de Sousa, J.T. (2004). Solving SAT with a Context-Switching Virtual Clause Pipeline and an FPGA Embedded Processor. In: Becker, J., Platzner, M., Vernalde, S. (eds) Field Programmable Logic and Application. FPL 2004. Lecture Notes in Computer Science, vol 3203. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30117-2_36
Download citation
DOI: https://doi.org/10.1007/978-3-540-30117-2_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22989-6
Online ISBN: 978-3-540-30117-2
eBook Packages: Springer Book Archive