Abstract
Boolean satisability (SAT), known as an NP-complete problem, has many important applications. The current generation of software SAT solvers implement non-chronological backtracking and clause recording to improve their performance. However, most hardware SAT solvers do not implement these methods since the methods require a complex process to work. To hasten the solving process compared with a contemporary software SAT solver, hardware SAT solvers need to implement these methods. In this paper, we show a method for implementing these methods without a complex process and design a hardware SAT solver using this method. The experimental results indicate that it is possible to estimate a 24-80x speed increase compared with a contemporary software SAT solver in EDA problems based on a reasonable assumption.
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
Silva, L.M., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. Computers 48(5), 506–521 (1999)
Dandalis, A., Prasanna, V.K.: Run-Time Performance Optimization of an FPGA-Based Deduction Engine for SAT Solvers. ACM Trans. Design Automation of Electronic Systems 7(4), 547–562 (2002)
Zhong, P., et al.: 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)
Karypis, G., et al.: Multilevel hypergraph partitioning: Application in the vlsi domain. In: Proceedings of the Design and Automation Conference (1997)
Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Comm. ACM 5, 394–397 (1962)
Moskewicz, M., et al.: Chaff: Engineering an efficient SAT Solver. In: Proceedings of the Design Automation Conference (July 2001)
DIMACS satsiability benchmark suite, available at ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/benchmarks/cnf/
SAT 2002 competition benchmarks, available at http://www.satlib.org/
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Hiramoto, S., Nakanishi, M., Yamashita, S., Nakashima, Y. (2007). A Hardware SAT Solver Using Non-chronological Backtracking and Clause Recording Without Overheads. In: Diniz, P.C., Marques, E., Bertels, K., Fernandes, M.M., Cardoso, J.M.P. (eds) Reconfigurable Computing: Architectures, Tools and Applications. ARC 2007. Lecture Notes in Computer Science, vol 4419. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71431-6_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-71431-6_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71430-9
Online ISBN: 978-3-540-71431-6
eBook Packages: Computer ScienceComputer Science (R0)