Abstract
In recent years, dynamic local search (DLS) clause weighting algorithms have emerged as the local search state-of-the-art for solving propositional satisfiability problems. However, most DLS algorithms require the tuning of domain dependent parameters before their performance becomes competitive. If manual parameter tuning is impractical then various mechanisms have been developed that can automatically adjust a parameter value during the search. To date, the most effective adaptive clause weighting algorithm is RSAPS. However, RSAPS is unable to convincingly outperform the best non-weighting adaptive algorithm AdaptNovelty + , even though manually tuned clause weighting algorithms can routinely outperform the Novelty + heuristic on which AdaptNovelty + is based.
In this study we introduce R+DDFW + , an enhanced version of the DDFW clause weighting algorithm developed in 2005, that not only adapts the total amount of weight according to the degree of stagnation in the search, but also incorporates the latest resolution-based preprocessing approach used by the winner of the 2005 SAT competition (R+ AdaptNovelty + ). In an empirical study we show R+DDFW + improves on DDFW and outperforms the other leading adaptive (R+Adapt-Novelty + , R+RSAPS) and non-adaptive (R+G2WSAT) local search solvers over a range of random and structured benchmark problems.
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
Morris, P.: The Breakout method for escaping from local minima. In: Proceedings of 11th AAAI, pp. 40–45 (1993)
Cha, B., Iwama, K.: Adding new clauses for faster local search. In: Proceedings of 13th AAAI, pp. 332–337 (1996)
Frank, J.: Learning short-term clause weights for GSAT. In: Proceedings of 15th IJCAI, pp. 384–389 (1997)
McAllester, D., Selman, B., Kautz, H.: Evidence for invariants in local search. In: Proceedings of 14th AAAI, pp. 321–326 (1997)
Wu, Z., Wah, B.: An efficient global-search strategy in discrete Lagrangian methods for solving hard satisfiability problems. In: Proceedings of 17th AAAI, pp. 310–315 (2000)
Schuurmans, D., Southey, F.: Local search characteristics of incomplete SAT procedures. In: Proceedings of 10th AAAI, pp. 297–302 (2000)
Hutter, F., Tompkins, D., Hoos, 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)
Thornton, J., Pham, D.N., Bain, S., Ferreira Jr., V.: Additive versus multiplicative clause weighting for SAT. In: Proceedings of 19th AAAI, pp. 191–196 (2004)
Hoos, H.: An adaptive noise mechanism for WalkSAT. In: Proceedings of 19th AAAI, pp. 655–660 (2002)
Ishtaiwi, A., Thornton, J., Sattar, A., Pham, D.N.: Neighbourhood clause weight redistribution in local search for SAT. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 772–776. Springer, Heidelberg (2005)
Schuurmans, D., Southey, F., Holte, R.: The exponentiated subgradient algorithm for heuristic boolean programming. In: Proceedings of 17th IJCAI, pp. 334–341 (2001)
Anbulagan, Pham, D., Slaney, J., Sattar, A.: Old resolution meets modern SLS. In: Proceedings of 20th AAAI, pp. 354–359 (2005)
Li, C.M., Huang, W.: Diversification and determinism in local search for satisfiability. In: Proceedings of 8th SAT, pp. 158–172 (2005)
Mills, P., Tsang, E.: Guided local search applied to the satisfiability (SAT) problem. In: Proceedings of 15th ASOR, pp. 872–883 (1999)
Thornton, J.: Clause weighting local search for SAT. Journal of Automated Reasoning (to appear, 2006)
Hutter, F., Hamadi, Y.: Parameter adjustment based on performance prediction: Towards an instance aware problem solver. Technical Report: MSR-TR-2005-125, Microsoft Research, WA (2005)
Li, C.M., Anbulagan: Look-ahead versus look-back for satisfiability problems. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 341–355. Springer, Heidelberg (1997)
Quine, W.V.: A way to simplify truth functions. American Mathematical Monthly 62, 627–631 (1955)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12, 23–41 (1965)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ishtaiwi, A., Thornton, J., Anbulagan, Sattar, A., Pham, D.N. (2006). Adaptive Clause Weight Redistribution. In: Benhamou, F. (eds) Principles and Practice of Constraint Programming - CP 2006. CP 2006. Lecture Notes in Computer Science, vol 4204. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11889205_18
Download citation
DOI: https://doi.org/10.1007/11889205_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-46267-5
Online ISBN: 978-3-540-46268-2
eBook Packages: Computer ScienceComputer Science (R0)