Advertisement

Frontiers of Computer Science

, Volume 13, Issue 1, pp 86–98 | Cite as

Empirical investigation of stochastic local search for maximum satisfiability

  • Yi Chu
  • Chuan Luo
  • Shaowei Cai
  • Haihang YouEmail author
Research Article
  • 14 Downloads

Abstract

The maximum satisfiability (MAX-SAT) problem is an important NP-hard problem in theory, and has a broad range of applications in practice. Stochastic local search (SLS) is becoming an increasingly popular method for solving MAX-SAT. Recently, a powerful SLS algorithm called CCLS shows efficiency on solving random and crafted MAX-SAT instances. However, the performance of CCLS on solving industrial MAX-SAT instances lags far behind. In this paper, we focus on experimentally analyzing the performance of SLS algorithms for solving industrial MAX-SAT instances. First, we conduct experiments to analyze why CCLS performs poor on industrial instances. Then we propose a new strategy called additive BMS (Best from Multiple Selections) to ease the serious issue. By integrating CCLS and additive BMS, we develop a new SLS algorithm for MAX-SAT called CCABMS, and related experiments indicate the efficiency of CCABMS. Also, we experimentally analyze the effectiveness of initialization methods on SLS algorithms for MAX-SAT, and combine an effective initialization method with CCABMS, resulting in an enhanced algorithm. Experimental results show that our enhanced algorithm performs better than its state-of-the-art SLS competitors on a large number of industrial MAX-SAT instances.

Keywords

empirical investigation stochastic local search maximum satisfiability industrial instances additive BMS 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Notes

Acknowledgements

This work was partially supported by the National Key Research and Development Program of China (2016YFE0100300, 2017YFB02025), partially supported by the 100 Talents Program of the Chinese Academy of Sciences (2920154070), partially supported by the Knowledge Innovation Project of the Chinese Academy of Sciences (5120146040), partially supported by the Open Project Program of the State Key Laboratory of Mathematical Engineering and Advanced Computing (2016A06), partially supported by the National Natural Science Foundation of China (Grant No. 61502464).

Supplementary material

11704_2018_7107_MOESM1_ESM.ppt (368 kb)
Supplementary material, approximately 366 KB.

References

  1. 1.
    Prestwich S D. CNF encodings. Handbook of Satisfiability. 2009, 75–97Google Scholar
  2. 2.
    Li C M, Manyà F. MaxSAT, hard and soft constraints. Handbook of Satisfiability, 2009, 185: 613–631Google Scholar
  3. 3.
    Smyth K, Hoos H H, Stützle T. Iterated robust tabu search for MAX-SAT. In: Proceedings of Conference of the Canadian Society for Computational Studies of Intelligence. 2003, 129–144Google Scholar
  4. 4.
    Yang Q, Wu K, Jiang Y. Learning action models from plan examples using weighted MAX-SAT. Artificial Intelligence, 2007, 171(2–3): 107–143MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Chen Y, Safarpour S, Marques-Silva J, Veneris A G. Automated design debugging with maximum satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2010, 29(11): 1804–1817CrossRefGoogle Scholar
  6. 6.
    Demirovic E, Musliu N. MaxSAT-based large neighborhood search for high school timetabling. Computers & Operations Research, 2017, 78: 172–180MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Huang W, Kitchaev D A, Dacek S, Rong Z Q, Urban A, Cao S, Luo C, Ceder G. Finding and proving the exact ground state of a generalized Ising model by convex optimization and MAX-SAT. Physical Review B, 2016, 94(13): 134424CrossRefGoogle Scholar
  8. 8.
    Berg J, Järvisalo M, Malone B. Learning optimal bounded treewidth bayesian networks via maximum satisfiability. Artifical Intelligence and Statistics. 2014, 86–95Google Scholar
  9. 9.
    Chieu H L, Lee W S. Relaxed survey propagation for the weighted maximum satisfiability problem. Journal of Artificial Intelligence Research, 2009, 36: 229–266MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Luo C, Cai S, Su K, Huang W. CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability. Artificial Intelligence, 2017, 243: 26–44MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Lin H, Su K. Exploiting inference rules to compute lower bounds for MAX-SAT solving. In: Proceedings of IJCAI. 2007, 2334–2339Google Scholar
  12. 12.
    Lin H, Su K, Li C M. Within-problem learning for efficient lower bound computation in Max-SAT solving. In: Proceedings of AAAI. 2008, 351–356Google Scholar
  13. 13.
    Li C M, Manyà F, Mohamedou N O, Planes J, Exploiting cycle structures in Max-SAT. In: Proceedings of International Conference on Theory and Applications of Satisfiability Testing. 2009, 467–480zbMATHGoogle Scholar
  14. 14.
    Ansótegui C, Bonet M L, Levy J. SAT-based MaxSAT algorithms. Artificial Intelligence, 2013, 196: 77–105MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Ansótegui C, Bonet M L, Gabàs J, Levy J. Improving WPM2 for (weighted) partial MaxSAT. In: Proceedings of International Conference on Principles and Practice of Constraint Programming. 2013, 117–132CrossRefGoogle Scholar
  16. 16.
    Narodytska N, Bacchus F. Maximum satisfiability using core-guided MaxSAT resolution. In: Proceedings of AAAI. 2014, 2717–2723Google Scholar
  17. 17.
    Hoos H H, Stützle T. Stochastic Local Search: Foundations & Applications. San Francisoc: Morgan Kaufmann, 2004zbMATHGoogle Scholar
  18. 18.
    Cai S, Luo C, Thornton J, Su K. Tailoring local search for partial MaxSAT. In: Proceedings of AAAI. 2014, 2623–2629Google Scholar
  19. 19.
    Cai S, Su K, Luo C, Sattar A. NuMVC: an efficient local search algorithm for minimum vertex cover. Journal of Artificial Intelligence Research, 2013, 46: 687–716MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Cai S. Balance between complexity and quality: local search for minimum vertex cover in massive graphs. In: Proceedings of IJCAI. 2015, 747–753Google Scholar
  21. 21.
    Zhang Z, He H, Luo Z, Qin H, Guo S. An efficient forest-based tabu search algorithm for the split-delivery vehicle routing problem. In: Proceedings of AAAI. 2015, 3432–3438Google Scholar
  22. 22.
    Umetani S. Exploiting variable associations to configure efficient local search in large-scale set partitioning problems. In: Proceedings of AAAI. 2015, 1226–1232Google Scholar
  23. 23.
    Lin J, Luo C, Cai S, Su K, Hao D, Zhang L. TCA: an efficient two-mode meta-heuristic algorithm for combinatorial test generation. In: Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2015, 494–505Google Scholar
  24. 24.
    Guo W, Liu G, Chen G, Peng S. A hybrid multi-objective pso algorithm with local search strategy for vlsi partitioning. Frontiers of Computer Science, 2014, 8(2): 203–216MathSciNetCrossRefGoogle Scholar
  25. 25.
    Selman B, Levesque H J, Mitchell D G. A new method for solving hard satisfiability problems. In: Proceedings of AAAI. 1992, 440–446Google Scholar
  26. 26.
    Selman B, Kautz H A, Cohen B. Noise strategies for improving local search. In: Proceedings of AAAI. 1994, 337–343Google Scholar
  27. 27.
    Jiang Y, Kautz H, Selman B. Solving problems with hard and soft constraints using a stochastic algorithm for MAX-SAT. In: Proceedings of the 1st International Joint Workshop on Artificial Intelligence and Operations Research. 1995, 20Google Scholar
  28. 28.
    Wah B W, Shang Y. Discrete lagrangian-based search for solving MAX-SAT problems. In: Proceedings of IJCAI. 1997, 378–383Google Scholar
  29. 29.
    Mills P, Tsang E P K. Guided local search for solving SAT and weighted MAX-SAT problems. Journal of Automated Reasoning, 2000, 24(1/2): 205–223MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Yagiura M, Ibaraki T. Efficient 2 and 3-flip neighborhood search algorithms for the MAX SAT: experimental evaluation. Journal of Heuristics, 2001, 7(5): 423–442CrossRefzbMATHGoogle Scholar
  31. 31.
    Sadowski K L, Bosman P A N, Thierens D. On the usefulness of linkage processing for solving MAX-SAT. In: Proceedings of GECCO. 2013, 853–860Google Scholar
  32. 32.
    Hains D, Whitley D, Howe A E, Chen W. Hyperplane initialized local search for MAX-SAT. In: Proceedings of the 15th Annual Conference on Genetic and Evolutionary Computation. 2013, 805–812Google Scholar
  33. 33.
    Whitley D, Howe A E, Hains D. Greedy or not? best improving versus first improving stochastic local search for MAX-SAT. In: Proceedings of AAAI. 2013, 940–946Google Scholar
  34. 34.
    Kroc L, Sabharwal A, Gomes C P, Selman B. Integrating systematic and local search paradigms: a new strategy for MaxSAT. In: Proceedings of IJCAI. 2009, 544–551Google Scholar
  35. 35.
    Cai S, Su K. Local search for Boolean satisfiability with configuration checking and subscore. Artificial Intelligence, 2013, 204: 75–98CrossRefzbMATHGoogle Scholar
  36. 36.
    Luo C, Cai S, Wu W, Jie Z, Su K. CCLS: an efficient local search algorithm for weighted maximum satisfiability. IEEE Transactions on Computers, 2015, 64(7): 1830–1843MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    Goffinet J, Ramanujan R. Monte-carlo tree search for the maximum satisfiability problem. In: Proceedings of International Conference on Principles and Practice of Constraint Programming. 2016, 251–267CrossRefGoogle Scholar
  38. 38.
    Wagner M. MaxSAT solver SC2016. Max-SAT Evaluation, 2016Google Scholar
  39. 39.
    Fan Y, Ma Z, Su K, Sattar A, Li C. Ramp: a local search solver based on make-positive variables. Max-SAT Evaluation, 2016Google Scholar
  40. 40.
    Cai S, Luo C, Lin J, Su K. New local search methods for partial maxsat. Artificial Intelligence, 2016, 240: 1–18MathSciNetCrossRefzbMATHGoogle Scholar
  41. 41.
    Roussel O. Controlling a solver execution with the runsolver tool. Journal on Satisfiability, Boolean Modeling and Computation, 2011, 7(4): 139–144MathSciNetzbMATHGoogle Scholar
  42. 42.
    Cai S, Lin J. Fast solving maximum weight clique problem in massive graphs. In: Proceedings of IJCAI. 2016, 568–574Google Scholar
  43. 43.
    Wang Y, Cai S, Yin M. Two efficient local search algorithms for maximum weight clique problem. In: Proceedings of AAAI. 2016, 805–811Google Scholar
  44. 44.
    Hutter F, Hoos H H, Leyton-Brown K, Stützle T. ParamILS: an automatic algorithm configuration framework. Journal of Artificial Intelligence Research, 2009, 36: 267–306CrossRefzbMATHGoogle Scholar
  45. 45.
    Hutter F, Hoos H H, Leyton-Brown K. Sequential model-based optimization for general algorithm configuration. In: Proceedings of Inter national Conference on Learning and Intelligent Optimization. 2011, 507–523CrossRefGoogle Scholar
  46. 46.
    Hoos H H. An adaptive noise mechanism for WalkSAT. In: Proceedings of AAAI. 2002, 655–660Google Scholar
  47. 47.
    Thornton J, Pham D N, Bain S, Ferreira Jr V. Additive versus multiplicative clause weighting for SAT. In: Proceedings of AAAI. 2004, 191–196Google Scholar

Copyright information

© Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  1. 1.State Key Laboratory of Computer Architecture, Institute of Computing TechnologyChinese Academy of SciencesBeijingChina
  2. 2.University of Chinese Academy of SciencesBeijingChina
  3. 3.State Key Laboratory of Mathematical Engineering and Advanced ComputingWuxiChina
  4. 4.State Key Laboratory of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingChina

Personalised recommendations