Abstract
We introduce in this paper a lightweight technique for reducing work repetition caused by non–chronological backtracking commonly practiced by DPLL–based SAT solvers. The presented technique can be viewed as a partial component caching scheme. Empirical evaluation of the technique reveals significant improvements on a broad range of industrial instances.
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
Aloul, F., Markov, I., Sakallah, K.: Force: a fast and easy-to-implement variable-ordering heuristic. In: Proc. of the 13th ACM Great Lakes Symposium on VLSI 2003, pp. 116–119 (2003)
Bayardo Jr., R.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: AAAI’97, Providence, Rhode Island, pp. 203–208 (1997), citeseer.ist.psu.edu/article/bayardo97using.html
Beame, P., et al.: Memoization and dpll: Formula caching proof systems. In: Proc. of 18th Annual IEEE Conf. on Computational Complexity, Aarhus, Denmark, IEEE Computer Society Press, Los Alamitos (2003), citeseer.ist.psu.edu/beame03memoization.html
Biere, A., Sinz, C.: Decomposing sat problems into connected components. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 2 (2006)
Darwiche, A.: New advances in compiling CNF to decomposable negational normal form. In: Proc. of European Conference on AI (2004)
Durairaj, V., Kalla, P.: Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 415–422. Springer, Heidelberg (2005)
Eén, N., Sörensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, Springer, Heidelberg (2004)
Ginsberg, M.L.: Dynamic backtracking. Jrnl of Artf. Intel. Resrh. 1, 25–46 (1993), ftp://ftp.cirl.uoregon.edu/pub/users/ginsberg/papers/dynamic.ps.gz
Huang, J., Darwiche, A.: A structure-based variable ordering heuristic for sat. In: IJCAI’03, Acapulco, Mexico, pp. 1167–1172 (2003)
IBM: Ibm formal verification benchmark library, http://www.research.ibm.com/haifa/projects/verification/RB_Homepage/fvbenchmarks.html
Marques-Silva, J.P., Sakallah, K.A.: GRASP - A New Search Algorithm for Satisfiability. In: Proceedings of IEEE/ACM International Conference on Computer-Aided Design, pp. 220–227. IEEE Computer Society Press, Los Alamitos (1996), citeseer.ist.psu.edu/article/marques-silva96grasp.html
Pipatsrisawat, K., Darwiche, A.: SAT Solver Description: RSat
Roberto, J., Bayardo, J., Pehoushek, J.D.: Counting models using connected components. In: Proc. of the 17th Natl. Conf. on AI, pp. 157–162. AAAI Press, Menlo Park (2000)
Rsat sat solver homepage, http://reasoning.cs.ucla.edu/rsat
Sang, T., et al.: Combining component caching and clause learning for effective model counting. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, Springer, Heidelberg (2005)
Beame, P., Kautz, H., Sang, T.: Heuristics for Fast Exact Model Counting. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 226–240. Springer, Heidelberg (2005)
SAT’05 Competition Homepage, http://www.satcompetition.org/2005/
Stallman, R.M., Sussman, G.J.: Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artf. Intel. 9 (1977)
Velev, M. N.: Sat benchmark lib, www.miroslav-velev.com/sat_benchmarks.html
Zhang, L., et al.: Efficient conflict driven learning in boolean satisfiability solver. In: ICCAD, pp. 279–285 (2001), citeseer.ist.psu.edu/article/zhang01efficient.html
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Pipatsrisawat, K., Darwiche, A. (2007). A Lightweight Component Caching Scheme for Satisfiability Solvers. In: Marques-Silva, J., Sakallah, K.A. (eds) Theory and Applications of Satisfiability Testing – SAT 2007. SAT 2007. Lecture Notes in Computer Science, vol 4501. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72788-0_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-72788-0_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72787-3
Online ISBN: 978-3-540-72788-0
eBook Packages: Computer ScienceComputer Science (R0)