Abstract
This paper presents a report on a new approach for solving satisfiability problems (SAT), i.e., creating a specialized logic circuit to solve each problem instance on Field Programmable Gate Arrays (FP-GAs). Recently, due to advances in FPGA technologies, users can now create their own reconfigurable logic circuits. Furthermore, by using current automatic logic synthesis technologies, users are able to design logic circuits automatically using a high level hardware description language (HDL). The combination of these two technologies have enabled users to rapidly create logic circuits specialized for solving individual problem instances. Satisfiability problems (SAT) were chosen because they make up an important subclass of NP-hard problems. We have developed a new algorithm called parallel-checking, which is suitable for this approach. In the algorithm, all variable values are assigned simultaneously, and all constraints are checked concurrently. Simulation results show that the order of the search tree size in this algorithm is approximately the same as that in the Davis-Putnam procedure. Then, we show how the parallel-checking algorithm can be implemented on FPGAs.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Brown, S. D., Francis, R. J., Rose, J., and Vranesic, Z. G.: Field-Programmable Gate Arrays, Kluwer Academic Publishers (1992).
Camposano, R. and Wolf, W.: High-Level VLSI Synthesis, Kluwer Academic Publishers (1991).
Nakamura, Y., Oguri, K., Nagoya A., Yukishita M., and Nomura R.: High-level synthesis design at NTT Systems Labs, IEICE Trans. Inf & Syst., Vol. E76-D, No.9, pp. 1047–1054 (1993).
Mackworth, A. K.: Constraint satisfaction, in Shapiro, S. C., ed., Encyclopedia of Artificial Intelligence, pp. 285–293, Wiley-Interscience Publication, New York (1992), second edition.
Cook, S.: The complexity of theorem proving procedures, Proceedings of the 3rd Annual ACM Symposium on the Theory of Computation, pp. 151–158 (1971).
Davis, M. and Putnam, H.: A computing procedure for quantification theory, Journal of the ACM, Vol. 7, pp. 201–215 (1960).
Mitchell, D., Selman, B., and Levesque, H.: Hard and easy distributions of SAT problem, Proceedings of the Tenth National Conference on Artificial Intelligence, pp. 459–465 (1992).
Zycad Corp.: Paradigm RP Concept Silicon User's Guide, Hardware Reference Manual, Software Reference Manual (1994).
Crawford, J. M. and Auton, L. D.: Experimental results on the crossover point in satisfiability problems, Proceedings of the Eleventh National Conference on Artificial Intelligence, pp. 21–27 (1993).
Freeman, J. W.: Improvements to propositional satisfiability search algorithms, PhD thesis, the University of Pennsylvania (1995).
Dubois, O., Andre, P., Boufkhad, Y., and Carlier, J.: SAT versus UNSAT, Proceedings of the DIMACS Challenge II Workshop (1993).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Suyama, T., Yokoo, M., Sawada, H. (1996). Solving satisfiability problems on FPGAs. In: Hartenstein, R.W., Glesner, M. (eds) Field-Programmable Logic Smart Applications, New Paradigms and Compilers. FPL 1996. Lecture Notes in Computer Science, vol 1142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61730-2_14
Download citation
DOI: https://doi.org/10.1007/3-540-61730-2_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61730-3
Online ISBN: 978-3-540-70670-0
eBook Packages: Springer Book Archive