Abstract
One way to design a local search algorithm that is effective on many types of instances is allowing this algorithm to switch among heuristics. In this paper, we refer to the way in which non-weighting algorithm adaptG 2 WSAT + selects a variable to flip, as heuristic adaptG 2 WSAT +, the way in which clause weighting algorithm RSAPS selects a variable to flip, as heuristic RSAPS, and the way in which variable weighting algorithm VW selects a variable to flip, as heuristic VW. We propose a new switching criterion: the evenness or unevenness of the distribution of clause weights. We apply this criterion, along with another switching criterion previously proposed, to heuristic adaptG 2 WSAT +, heuristic RSAPS, and heuristic VW. The resulting local search algorithm, which adaptively switches among these three heuristics in every search step according to these two criteria to intensify or diversify the search when necessary, is called NCVW (Non-, Clause, and Variable Weighting). Experimental results show that NCVW is generally effective on a wide range of instances while adaptG 2 WSAT +, RSAPS, VW, and gNovelty + and adaptG 2 WSAT0, which won the gold and silver medals in the satisfiable random category in the SAT 2007 competition, respectively, are not.
The work of the first author is partially supported by NSERC PGS-D (Natural Sciences and Engineering Research Council of Canada Post-Graduate Scholarships for Doctoral students).
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.
Similar content being viewed by others
References
Gebruers, C., Hnich, B., Bridge, D.G., Freuder, E.C.: Using CBR to Select Solution Strategies in Constraint Programming. In: Muñoz-Ávila, H., Ricci, F. (eds.) ICCBR 2005. LNCS (LNAI), vol. 3620, pp. 222–236. Springer, Heidelberg (2005)
Hirsch, E.A., Kojevnikov, A.: UnitWalk: A New SAT Solver that Uses Local Search Guided by Unit Clause Elimination. Ann. Math. Artif. Intell. 43(1), 91–111 (2005)
Hoos, H.H.: On the Run-Time Behavior of Stochastic Local Search Algorithms for SAT. In: Proceedings of AAAI 1999, pp. 661–666. AAAI Press, Menlo Park (1999)
Hoos, H.H.: An Adaptive Noise Mechanism for WalkSAT. In: Proceedings of AAAI 2002, pp. 655–660. AAAI Press, Menlo Park (2002)
Hoos, H.H., Stűtzle, T.: Stochastic Local Search: Foundations and Applications. Morgan Kaufmann, San Francisco (2004)
Hutter, F., Tompkins, D.A.D., Hoos, H.H.: Scaling and Probabilistic Smoothing: Efficient Dynamical Local Search for SAT. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 233–248. Springer, Heidelberg (2002)
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)
Li, C.M., Wei, W., Zhang, H.: Combining Adaptive Noise and Promising Decreasing Variables in Local Search for SAT, http://www.satcompetition.org/2007/contestants.html
Li, C.M., Wei, W., Zhang, H.: Combining Adaptive Noise and Look-Ahead in Local Search for SAT. In: Benhamou, F., Jussien, N., O’Sullivan, B. (eds.) Trends in Constraint Programming, ch. 14, pp. 261–267. ISTE (2007)
Li, C.M., Wei, W., Zhang, H.: Combining Adaptive Noise and Look-Ahead in Local Search for SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 121–133. Springer, Heidelberg (2007)
Morris, P.: The Breakout Method for Escaping from Local Minima. In: Proceedings of AAAI 1993, pp. 40–45. AAAI Press, Menlo Park (1993)
Pham, D.N., Gretton, C.: gnovelty+, http://www.satcompetition.org/2007/contestants.html
Prestwich, S.: Random Walk with Continuously Smoothed Variable Weights. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 203–215. Springer, Heidelberg (2005)
Selman, B., Kautz, H., Cohen, B.: Noise Strategies for Improving Local Search. In: Proceedings of AAAI 1994, pp. 337–343. AAAI Press, Menlo Park (1994)
Wei, W., Li, C.M., Zhang, H.: Deterministic and Random Selection of Variables in Local Search for SAT, http://www.satcompetition.org/2007/contestants.html
Wei, W., Li, C.M., Zhang, H.: Criterion for Intensification and Diversification in Local Search for SAT. In: Proceedings of LSCS 2007, pp. 2–16 (2007)
Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla-07: 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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wei, W., Li, C.M., Zhang, H. (2008). Switching among Non-Weighting, Clause Weighting, and Variable Weighting in Local Search for SAT. In: Stuckey, P.J. (eds) Principles and Practice of Constraint Programming. CP 2008. Lecture Notes in Computer Science, vol 5202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85958-1_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-85958-1_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85957-4
Online ISBN: 978-3-540-85958-1
eBook Packages: Computer ScienceComputer Science (R0)