Advertisement

Tie Breaking in Clause Weighting Local Search for SAT

  • Valnir FerreiraJr.
  • John Thornton
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3809)

Abstract

Clause weighting local search methods are widely used for satisfiability testing. A feature of particular importance for such methods is the scheme used to maintain the clause weight distribution relevant to different areas of the search landscape. Existing methods periodically adjust clause weights either multiplicatively or additively. Tie breaking strategies are used whenever a method’s evaluation function encounters more than one optimal candidate flip, with the dominant approach being to break such ties randomly. Although this is acceptable for multiplicative methods as they rarely encounter such situations, additive methods encounter significantly more tie breaking scenarios in their landscapes, and therefore a more refined tie breaking strategy is of much greater relevance. This paper proposes a new way of handling the tie breaking situations frequently encountered in the landscapes of additive constraint weighting local search methods. We demonstrate through an empirical study that when this idea is used to modify the purely random tie breaking strategy of a state-of-the-art solver, the modified method significantly outperforms the existing one on a range of benchmarks, especially when we consider the encodings of large and structured problems.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Morris, P.: The breakout method for escaping from local minima. In: Proceedings of the 11th National Conference on Artificial Intelligence (AAAI 1993), pp. 40–45. MIT Press, Washington (1993)Google Scholar
  2. 2.
    Selman, B., Kautz, H.: Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI 1993), Chambery, France, pp. 290–295. Morgan Kaufmann, San Francisco (1993)Google Scholar
  3. 3.
    Wah, B., Shang, Y.: Discrete lagrangian-based search for solving MAX-SAT problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), Nagoya, Japan, pp. 378–383. Morgan Kaufmann, San Francisco (1997)Google Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Thornton, J., Pham, D.N., Bain, S., Ferreira Jr., V.: Additive versus multiplicative clause weighting for SAT. In: Proceedings of the 20th National Conference on Artificial Intelligence (AAAI 2004), San Jose, California, pp. 191–196. MIT Press, Cambridge (2004)Google Scholar
  6. 6.
    Hoos, H.H., Stützle, T.: Stochastic Local Search: Foundations and Applications. Morgan Kaufmann, San Francisco (2005)zbMATHGoogle Scholar
  7. 7.
    Schuurmans, D., Southey, F.: Local search characteristics of incomplete SAT procedures. In: Proceedings of the 1tth National Conference on Artificial Intelligence (AAAI 2000), Austin, TX, pp. 297–302. MIT Press, Cambridge (2000)Google Scholar
  8. 8.
    Selmann, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proceedings of the 12th National Conference on Artificial Intelligence (AAAI 1994), Seattle, WA, pp. 337–343. AAAI Press, Menlo Park (1994)Google Scholar
  9. 9.
    Prestwich, S.: Local search on sat-encoded CSPs. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 105–119. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  10. 10.
    Achlioptas, D., Gomes, C., Kautz, H., Selman, B.: Generating satisfiable problem instances. In: Proceedings of the 17th National Conference on Artificial Intelligence (AAAI 2000), Austin, TX, pp. 256–261. MIT Press, Cambridge (2000)Google Scholar
  11. 11.
    Kautz, H., Ruan, Y., Achlioptas, D., Gomes, C., Selman, B., Stickel, M.: Balance and filtering in structured satisfiable problems. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI 2001), Seattle, pp. 351–358. Morgan Kaufmann, San Francisco (2001)Google Scholar
  12. 12.
    Thornton, J.: Clause weighting local search for SAT. Journal of Artificial Intelligence Research (to appear)Google Scholar
  13. 13.
    Tompkins, D., Hoos, H.: Warped landscapes and random acts of SAT solving. In: Proceedings of the Eighth International Symposium on Artificial Intelligence and Mathematics - AMAI, AI&M 2004, Fort Lauderdale, Florida (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Valnir FerreiraJr.
    • 1
  • John Thornton
    • 1
  1. 1.Institute for Integrated and Intelligent SystemsGriffith UniversityQLD

Personalised recommendations