Abstract
Although clause weighting local search algorithms have produced some of the best results on a range of challenging satisfiability (SAT) benchmarks, this performance is dependent on the careful hand-tuning of sensitive parameters. When such hand-tuning is not possible, clause weighting algorithms are generally outperformed by self-tuning WalkSAT-based algorithms such as AdaptNovelty + and AdaptG2WSAT.
In this paper we investigate tuning the weight decay parameter of two clause weighting algorithms using the statistical properties of cost distributions that are dynamically accumulated as the search progresses. This method selects a parameter setting both according to the speed of descent in the cost space and according to the shape of the accumulated cost distribution, where we take the shape to be a predictor of future performance. In a wide ranging empirical study we show that this automated approach to parameter tuning can outperform the default settings for two state-of-the-art algorithms that employ clause weighting (PAWS and gNovelty + ). We also show that these self-tuning algorithms are competitive with three of the best-known self-tuning SAT local search techniques: RSAPS, AdaptNovelty + and AdaptG2WSAT.
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
Selman, B., Levesque, H., Mitchell, D.: A new method for solving hard satisfiability problems. In: Proceedings of AAAI 1992, pp. 440–446 (1992)
Li, C.M., Huang, W.Q.: Diversification and determinism in local search for satisfiability. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 158–172. Springer, Heidelberg (2005)
Wu, Z., Wah, B.: An efficient global-search strategy in discrete Lagrangian methods for solving hard satisfiability problems. In: Proceedings of AAAI 2000, pp. 310–315 (2000)
Hutter, F., Tompkins, D., Hoos, H.H.: Scaling and probabilistic smoothing: Efficient dynamic local search for SAT. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 233–248. Springer, Heidelberg (2002)
Mills, P., Tsang, E.: Guided local search applied to the satisfiability (SAT) problem. In: Proceedings of ASOR 1999, pp. 872–883 (1999)
Thornton, J.R., Pham, D.N., Bain, S., Ferreira Jr., V.: Additive versus multiplicative clause weighting for SAT. In: Proceedings of AAAI 2004, pp. 191–196 (2004)
Hoos, H.H.: An adaptive noise mechanism for WalkSAT. In: Proceedings of AAAI 2002, pp. 635–660 (2002)
Pham, D.N., Thornton, J.R., Gretton, C., Sattar, A.: Advances in local search for satisfiability. In: Orgun, M.A., Thornton, J. (eds.) AI 2007. LNCS (LNAI), vol. 4830, pp. 213–222. Springer, Heidelberg (2007)
Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: The design and analysis of an algorithm portfolio for SAT. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 712–727. Springer, Heidelberg (2007)
Gagliolo, M., Schmidhuber, J.: Dynamic algorithm portfolios. In: Proceedings of AI-MATH 2006 (2006)
Hutter, F., Hoos, H.H., Stützle, T.: Automatic algorithm configuration based on local search. In: Proceedings of AAAI 2007, pp. 1152–1157 (2007)
Birattari, M., Stützle, T., Paquete, L., Varrentrapp, K.: A racing algorithm for configuring metaheuristics. In: Proceedings of GECCO 2002, pp. 11–18 (2002)
Gomes, C.P., Selman, B.: Algorithm portfolios. Artificial Intelligence 126, 43–62 (2001)
Hutter, F., Hamadi, Y., Hoos, H.H., Leyton-Brown, K.: Performance prediction and automated tuning of randomized and parametric algorithms. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 213–228. Springer, Heidelberg (2006)
Carchrae, T., Beck, J.C.: Low-knowledge algorithm control. In: Proceedings of AAAI 2004, pp. 49–54 (2004)
Battiti, R., Protasi, M.: Reactive search, a history-sensitive heuristic for MAX-SAT. ACM Journal of Experimental Algorithmics 2(Article 2) (1997)
McAllester, D.A., Selman, B., Kautz, H.A.: Evidence for invariants in local search. In: Proceedings of AAAI 1997, pp. 321–326 (1997)
Thornton, J.: Clause weighting local search for SAT. Journal of Automated Reasoning 35(1-3), 97–142 (2005)
Kirkpatrick, S., Gelatt, C.D., Vecchi, M.P.: Optimization by simulated annealing. Science 220(4598), 671–680 (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thornton, J., Pham, D.N. (2008). Using Cost Distributions to Guide Weight Decay in Local Search for SAT. In: Ho, TB., Zhou, ZH. (eds) PRICAI 2008: Trends in Artificial Intelligence. PRICAI 2008. Lecture Notes in Computer Science(), vol 5351. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89197-0_38
Download citation
DOI: https://doi.org/10.1007/978-3-540-89197-0_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89196-3
Online ISBN: 978-3-540-89197-0
eBook Packages: Computer ScienceComputer Science (R0)