Abstract
We introduce an adaptive algorithm to control the use of the double look-ahead procedure. This procedure sometimes enhances the performance of look-ahead based satisfiability solvers. Current use of this procedure is driven by static heuristics. Experiments show that over a wide variety of instances, different parameter settings result in optimal performance. Moreover, a strategy that yields fast performance on one particular class of instances may cause a significant slowdown on other families. Using a single adaptive strategy, we accomplish performances close to the optimal performances reached by the various static settings. On some families, we clearly outperform even the fastest performance based on static heuristics. This paper provides a description of the algorithm and a comparison with the static strategies. This method is incorporated in march_dl, satz, and kcnfs. Also, the dynamic behavior of the algorithm is illustrated by adaptation plots on various benchmarks.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Biere, A., et al.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Connamacher, H.: A random constraint satisfaction problem that seems hard for DPLL. In: Proceedings of SAT (2004)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)
Dubois, O., Dequen, G.: source code of the kcnfs solver. Available at http://www.laria.u-picardie.fr/~dequen/sat/
Freeman, J.W.: Improvements to Propositional Satisfiability Search Algorithms. Ph.D. thesis, University of Pennsylvania, Philadelphia (1995)
Le Berre, D., Simon, L.: The essentials of the SAT’03 Competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 452–467. Springer, Heidelberg (2004)
Li, C.M.: A constraint-based approach to narrow search trees for satisfiability. Information processing letters 71, 75–80 (1999)
Li, C.M., Anbulagan: Heuristics Based on Unit Propagation for Satisfiability Problems. In: Proc. of Fifteenth IJCAI, pp. 366–371 (1997)
Simon, L., Le Berre, D., Hirsch, E.: The SAT 2002 competition. Annals of Mathematics and Artificial Intelligence (AMAI) 43, 343–378 (2005)
Simon, L.: Sat’04 competition homepage, http://www.satcompetition.org/2004
Zhang, H., Stickel, M.E.: Implementing the Davis-Putnam Method. In: SAT 2000, pp. 309–326 (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Heule, M., van Maaren, H. (2007). Effective Incorporation of Double Look-Ahead Procedures. 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_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-72788-0_25
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)