Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Focused Random Walk with Configuration Checking and Break Minimum for Satisfiability

  • Conference paper
Principles and Practice of Constraint Programming (CP 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8124))

Abstract

Stochastic local search (SLS) algorithms, especially those adopting the focused random walk (FRW) framework, have exhibited great effectiveness in solving satisfiable random 3-satisfiability (3-SAT) instances. However, they are still unsatisfactory in dealing with huge instances, and are usually sensitive to the clause-to-variable ratio of the instance. In this paper, we present a new FRW algorithm dubbed FrwCB, which behaves more satisfying in the above two aspects. The main idea is a new heuristic called CCBM, which combines a recent diversification strategy named configuration checking (CC) with the common break minimum (BM) variable-picking strategy. By combining CC and BM in a subtle way, CCBM significantly improves the performance of FrwCB, making FrwCB achieve state-of-the-art performance on a wide range of benchmarks. The experiments show that FrwCB significantly outperforms state-of-the-art SLS solvers on random 3-SAT instances, and competes well on random 5-SAT, random 7-SAT and structured instances.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aurell, E., Gordon, U., Kirkpatrick, S.: Comparing beliefs, surveys and random walks. Advances in Neural Information Processing Systems 17, 49–56 (2005)

    Google Scholar 

  2. Balint, A., Fröhlich, A.: Improving stochastic local search for SAT with a new probability distribution. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 10–15. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  3. Balint, A., Schöning, U.: Choosing probability distributions for stochastic local search and the role of make versus break. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 16–29. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Biere, A.: Lingeling and friends at the SAT competition 2011. Technical Report FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University (2011), http://fmv.jku.at/papers/Biere-FMV-TR-11-1.pdf

  5. Braunstein, A., Mézard, M., Zecchina, R.: Survey propagation: An algorithm for satisfiability. Random Struct. Algorithms 27(2), 201–226 (2005)

    Article  MATH  Google Scholar 

  6. Brüggemann, T., Kern, W.: An improved deterministic local search algorithm for 3-SAT. Theor. Comput. Sci. 329(1-3), 303–313 (2004)

    Article  MATH  Google Scholar 

  7. Cai, S., Su, K.: Local search with configuration checking for SAT. In: Proc. of ICTAI 2011, pp. 59–66 (2011)

    Google Scholar 

  8. Cai, S., Su, K.: Configuration checking with aspiration in local search for SAT. In: Proc. of AAAI 2012, pp. 434–440 (2012)

    Google Scholar 

  9. Cai, S., Su, K., Luo, C., Sattar, A.: NuMVC: An efficient local search algorithm for minimum vertex cover. J. Artif. Intell. Res (JAIR) 46, 687–716 (2013)

    MathSciNet  MATH  Google Scholar 

  10. Cai, S., Su, K., Sattar, A.: Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artif. Intell. 175(9-10), 1672–1696 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  11. Guo, W., Yang, G., Hung, W.N.N., Song, X.: Complete boolean satisfiability solving algorithms based on local search. J. Comput. Sci. Technol. 28(2), 247–254 (2013)

    Article  MathSciNet  Google Scholar 

  12. Hoos, H.H.: An adaptive noise mechanism for WalkSAT. In: Proc. of AAAI 2002, pp. 655–660 (2002)

    Google Scholar 

  13. Hoos, H.H., Stützle, T.: Systematic vs. local search for SAT. In: Proc. of KI 1999, pp. 289–293 (1999)

    Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. Järvisalo, M., Biere, A., Heule, M.: Simulating circuit-level simplifications on CNF. J. Autom. Reasoning 49(4), 583–619 (2012)

    Article  MATH  Google Scholar 

  16. Kirkpatrick, S., Selman, B.: Critical behavior in the satisfiability of random boolean formulae. Science 264, 1297–1301 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  17. Lewis, M.D.T., Schubert, T., Becker, B.W.: Speedup techniques utilized in modern SAT solvers. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 437–443. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. Li, C.M., Li, Y.: Satisfying versus falsifying in local search for satisfiability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 477–478. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  20. Luo, C., Su, K., Cai, S.: Improving local search for random 3-SAT using quantitative configuration checking. In: Proc. of ECAI 2012, pp. 570–575 (2012)

    Google Scholar 

  21. Papadimitriou, C.H.: On selecting a satisfying truth assignment. In: Proc. of FOCS 1991, pp. 163–169 (1991)

    Google Scholar 

  22. Parkes, A.J.: Scaling properties of pure random walk on random 3-SAT. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 708–713. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  23. Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proc. of AAAI 1994, pp. 337–343 (1994)

    Google Scholar 

  24. Selman, B., Levesque, H.J., Mitchell, D.G.: A new method for solving hard satisfiability problems. In: Proc. of AAAI 1992, pp. 440–446 (1992)

    Google Scholar 

  25. Tompkins, D.A.D., Balint, A., Hoos, H.H.: Captain jack: New variable selection heuristics in local search for SAT. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 302–316. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  26. Wei, W., Li, C.-M., Zhang, H.: Switching among non-weighting, clause weighting, and variable weighting in local search for SAT. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 313–326. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  27. Wu, Z., Wah, B.W.: An efficient global-search strategy in discrete lagrangian methods for solving hard satisfiability problems. In: Proc. of AAAI 2000, pp. 310–315 (2000)

    Google Scholar 

  28. Xu, K., Boussemart, F., Hemery, F., Lecoutre, C.: A simple model to generate hard satisfiable instances. In: Proc. of IJCAI 2005, pp. 337–342 (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Key Laboratory of High Confidence Software Technologies, Peking University, Beijing, China

    Chuan Luo & Wei Wu

  2. Queensland Research Laboratory, National ICT Australia, QLD, Australia

    Shaowei Cai

  3. College of Mathematics, Physics and Information Engineering, Zhejiang Normal University, Jinhua, China

    Wei Wu & Kaile Su

  4. Institute for Integrated and Intelligent Systems, Griffith University, Brisbane, Australia

    Kaile Su

Authors
  1. Chuan Luo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shaowei Cai
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wei Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Kaile Su
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Information and Communication Technology, KTH Royal Institute of Technology, P.O. Box Forum 120, 16440, Kista, Sweden

    Christian Schulte

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Luo, C., Cai, S., Wu, W., Su, K. (2013). Focused Random Walk with Configuration Checking and Break Minimum for Satisfiability. In: Schulte, C. (eds) Principles and Practice of Constraint Programming. CP 2013. Lecture Notes in Computer Science, vol 8124. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40627-0_37

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40627-0_37

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40626-3

  • Online ISBN: 978-3-642-40627-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation