Abstract
Many current local search algorithms for SAT fall into one of two classes. Random walk algorithms such as Walksat/SKC, Novelty+ and HWSAT are very successful but can be trapped for long periods in deep local minima. Clause weighting algorithms such as DLM, GLS, ESG and SAPS are good at escaping local minima but require expensive smoothing phases in which all weights are updated. We show that Walksat performance can be greatly enhanced by weighting variables instead of clauses, giving the best known results on some benchmarks. The new algorithm uses an efficient weight smoothing technique with no smoothing phase.
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
Asahiro, Y., Iwama, K., Miyano, E.: Random Generation of Test Instances with Controlled Attributes. In: Johnson, D.S., Trick, M.A. (eds.) Cliques, Coloring and Satisfiability: Second Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, pp. 127–154. American Mathematical Society, Providence (1996)
Cha, B., Iwama, K.: Performance Test of Local Search Algorithms Using New Types of Random CNF Formulas. In: Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, pp. 304–310. Morgan Kaufmann, San Francisco (1995)
Culberson, J., Gent, I.P., Hoos, H.H.: On the Probabilistic Approximate Completeness of WalkSAT for 2-SAT. Technical Report APES-15a-2000, APES Research Group (2000)
Frank, J.: Weighting for GODOT: Learning Heuristics for GSAT. In: Proceedings of the Thirteenth National Conference on Artificial Intelligence, pp. 338–343. MIT Press, Cambridge (1996)
Frank, J.: Learning Short-Term Weights for GSAT. In: Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, pp. 384–389. Morgan Kaufmann, San Francisco (1997)
Fukunaga, A.S.: Variable-Selection Heuristics in Local Search for SAT. In: Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, pp. 275–280 (1997)
Gent, I.P., Walsh, T.: Towards an Understanding of Hill-Climbing Procedures for SAT. In: Proceedings of the Eleventh National Conference on Artificial Intelligence, pp. 28–33. AAAI Press, Menlo Park (1993)
Gent, I.P., Walsh, T.: Unsatisfied Variables in Local Search. In: Hallam, J. (ed.) Hybrid Problems, Hybrid Solutions, pp. 73–85. IOS Press, Amsterdam (1995)
Ginsberg, M.L., Parkes, A.J.: Satisfiability Algorithms and Finite Quantification. In: Seventh International Conference on Principles of Knowledge Representation and Reasoning, pp. 690–701. Morgan Kaufmann, San Francisco (2000)
Gu, J.: Efficient Local Search for Very Large-Scale Satisfiability Problems. Sigart Bulletin 3(1), 8–12 (1992)
Hirsch, E.A., Kojevnikov, A.: Solving Boolean Satisfiability Using Local Search Guided by Unit Clause Elimination. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 605–609. Springer, Heidelberg (2001)
Hoos, H.H.: On the Run-Time Behaviour of Stochastic Local Search Algorithms. In: Sixteenth National Conference on Artificial Intelligence, pp. 661–666. AAAI Press, Menlo Park (1999)
Huang, W., Zhang, D., Wang, H.: An Algorithm Based on Tabu Search for Satisfiability Problem. Journal of Computer Science and Technology 17(3), Editorial Universitaria de Buenos Aires, 340–346 (2002)
Hutter, F., Tompkins, D.A.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)
Mazure, B., Saïs, L., Grégoire, É.: Tabu Search for SAT. In: Proceedings of the Fourteenth National Conference on Artificial Intelligence, pp. 281–285 (1997)
Mazure, B., Saïs, L., Grégoire, É.: Boosting Complete Techniques Thanks to Local Search. Annals of Mathematics and Artificial Intelligence 22, 309–322 (1998)
McAllester, D.A., Selman, B., Kautz, H.A.: Evidence for Invariants in Local Search. In: Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, pp. 321–326. AAAI Press / MIT Press (1997)
Mills, P., Tsang, E.P.K.: Guided Local Search for Solving SAT and Weighted MAX-SAT Problems. Journal of Automated Reasoning, Special Issue on Satisfiability Problems 24, 205–223 (2000)
Morris, P.: The Breakout Method for Escaping from Local Minima. In: Proceedings of the Eleventh National Conference on Artificial Intelligence, pp. 40–45. AAAI Press / MIT Press (1993)
Prestwich, S.D.: Incomplete Dynamic Backtracking for Linear Pseudo-Boolean Problems. Annals of Operations Research 130, 57–73 (2004)
Prestwich, S.D.: SAT Problems With Chains of Dependent Variables. Discrete Applied Mathematics 3037, 1–22 (2002)
Schuurmans, D., Southey, F., Holte, R.C.: The Exponentiated Subgradient Algorithm for Heuristic Boolean Programming. In: Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, pp. 334–341. Morgan Kaufmann, San Francisco (2001)
Schuurmans, D., Southey, F.: Local Search Characteristics of Incomplete SAT Procedures. In: Proceedings of the Seventeenth National Conference on Artificial Intelligence, pp. 297–302. AAAI Press, Menlo Park (2000)
Selman, B., Kautz, H.A.: Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems. In: Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence, pp. 290–295 (1993)
Selman, B., Kautz, H.A., Cohen, B.: Noise Strategies for Improving Local Search. In: Proceedings of the Twelfth National Conference on Artificial Intelligence, pp. 337–343. AAAI Press, Menlo Park (1994)
Selman, B., Levesque, H., Mitchell, D.: A New Method for Solving Hard Satisfiability Problems. In: Proceedings of the Tenth National Conference on Artificial Intelligence, pp. 440–446. MIT Press, Cambridge (1992)
Smyth, K., Hoos, H.H., Stützle, T.: Iterated Robust Tabu Search for MAX-SAT. In: Xiang, Y., Chaib-draa, B. (eds.) Canadian AI 2003. LNCS (LNAI), vol. 2671, pp. 129–144. Springer, Heidelberg (2003)
Thornton, J.R., Pullan, W., Terry, J.: Towards Fewer Parameters for Clause Weighting SAT Algorithms. In: McKay, B., Slaney, J.K. (eds.) Canadian AI 2002. LNCS (LNAI), vol. 2557, pp. 569–578. Springer, Heidelberg (2002)
Thornton, J.R., Pham, D.N., Bain, S., Ferreira Jr., V.: Additive versus Multiplicative Clause Weighting for SAT. In: Proceedings of the Nineteenth National Conference on Artificial Intelligence, San Jose, California, pp. 191–196 (2004)
Tompkins, D.A.D., Hoos, H.H.: UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 37–46. Springer, Heidelberg (2005)
Tompkins, D.A.D., Hoos, H.H.: Scaling and Probabilistic Smoothing: Dynamic Local Search for Unweighted MAX-SAT. In: Xiang, Y., Chaib-draa, B. (eds.) Canadian AI 2003. LNCS (LNAI), vol. 2671, pp. 145–159. Springer, Heidelberg (2003)
Tompkins, D.A.D., Hoos, H.H.: Warped Landscapes and Random Acts of SAT Solving. In: Proceedings of the Eighth International Symposium on Artificial Intelligence and Mathematics (2004) (to appear)
Wei, W., Selman, B.: Accelerating Random Walks. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 216–232. Springer, Heidelberg (2002)
Wu, Z., Wah, B.W.: An Efficient Global-Search Strategy in Discrete Lagrangian Methods for Solving Hard Satisfiability Problems. In: Proceedings of the Seventeenth National Conference on Artificial Intelligence, pp. 310–315. AAAI Press, Menlo Park (2000)
Zhang, W., Rangan, A., Looks, M.: Backbone Guided Local Search for Maximum Satisfiability. In: Eighteenth International Joint Conference on Artificial Intelligence, pp. 1179–1186 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Prestwich, S. (2005). Random Walk with Continuously Smoothed Variable Weights. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_15
Download citation
DOI: https://doi.org/10.1007/11499107_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)