Document Open Access Logo

Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme

Authors Yi Chu , Chu-Min Li , Furong Ye , Shaowei Cai

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.8.pdf
  • Filesize: 0.83 MB
  • 18 pages

Document Identifiers

Author Details

Yi Chu
  • Institute of Software, Chinese Academy of Sciences, Beijing, China
Chu-Min Li
  • MIS, UR 4290, Université de Picardie Jules Verne, Amiens, France
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
Furong Ye
  • Key Laboratory of System Software, Chinese Academy of Sciences, Beijing, China
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
Shaowei Cai
  • Key Laboratory of System Software, Chinese Academy of Sciences, Beijing, China
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

Funding

This work was supported by the National Natural Science Foundation of China under Grant 62302492, and the French Agence Nationale de la Recherche, via AI chair ANR-19-CHIA- 0013-01 (Massal’IA).

Cite As Get BibTex

Yi Chu, Chu-Min Li, Furong Ye, and Shaowei Cai. Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.SAT.2024.8

Abstract

Local search has been widely applied to solve the well-known (weighted) partial MaxSAT problem, significantly influencing many real-world applications. The main difficulty to overcome when designing a local search algorithm is that it can easily fall into local optima. Clause weighting is a beneficial technique that dynamically adjusts the landscape of search space to help the algorithm escape from local optima. Existing works tend to increase the weights of falsified clauses, and such strategies may result in an unpredictable landscape of search space during the optimization process. Therefore, in this paper, we propose a Unified Soft Clause Weighting Scheme called Unified-SW, which increases the weights of all soft clauses in feasible local optima, whether they are satisfied or not, while preserving the hierarchy among them. We implemented Unified-SW in a new local search solver called USW-LS. Experimental results demonstrate that USW-LS, outperforms the state-of-the-art local search solvers across benchmarks from anytime tracks of recent MaxSAT Evaluations. More promisingly, a hybrid solver combining USW-LS and TT-Open-WBO-Inc won all four categories in the anytime track of MaxSAT Evaluation 2023.

Subject Classification

ACM Subject Classification
  • Theory of computation → Randomized local search
Keywords
  • Weighted Partial MaxSAT
  • Local Search Method
  • Weighting Scheme

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. André Abramé and Djamal Habet. Ahmaxsat: Description and evaluation of a branch and bound max-sat solver. Journal on Satisfiability, Boolean Modeling and Computation, 9(1):89-128, 2014. Google Scholar
  2. David Allouche, Isabelle André, Sophie Barbe, Jessica Davies, Simon de Givry, George Katsirelos, Barry O'Sullivan, Steve Prestwich, Thomas Schiex, and Seydou Traoré. Computational protein design as an optimization problem. Artificial Intelligence, 212:59-79, 2014. Google Scholar
  3. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. Solving (weighted) partial maxsat through satisfiability testing. In Proceedings of SAT 2009, pages 427-440. Springer, 2009. Google Scholar
  4. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. A new algorithm for weighted partial maxsat. In Proceedings of AAAI 2010, pages 3-8, 2010. Google Scholar
  5. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. Artificial Intelligence, 196:77-105, 2013. Google Scholar
  6. Carlos Ansótegui and Joel Gabàs. WPM3: An (in)complete algorithm for weighted partial MaxSAT. Artificial Intelligence, 250:37-57, 2017. Google Scholar
  7. Gilles Audemard and Laurent Simon. On the glucose sat solver. International Journal on Artificial Intelligence Tools, 27(01):1840001, 2018. Google Scholar
  8. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiabiliy. In Handbook of satisfiability, pages 929-991. IOS Press, 2021. Google Scholar
  9. Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified core-guided maxsat solving. In International Conference on Automated Deduction, pages 1-22. Springer, 2023. Google Scholar
  10. Jeremias Berg, Emir Demirovic, and Peter J. Stuckey. Core-boosted linear search for incomplete MaxSAT. In Proceedings of CPAIOR 2019, pages 39-56, 2019. Google Scholar
  11. Shaowei Cai. Balance between complexity and quality: Local search for minimum vertex cover in massive graphs. In Proceedings of IJCAI 2015, pages 747-753, 2015. Google Scholar
  12. Shaowei Cai and Zhendong Lei. Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability. Artificial Intelligence, 287:103354, 2020. Google Scholar
  13. Shaowei Cai, Chuan Luo, Jinkun Lin, and Kaile Su. New local search methods for partial MaxSAT. Artificial Intelligence, 240:1-18, 2016. Google Scholar
  14. Shaowei Cai, Chuan Luo, John Thornton, and Kaile Su. Tailoring local search for partial maxsat. In Proceedings of AAAI 2014, pages 2623-2629, 2014. Google Scholar
  15. Byungki Cha, Kazuo Iwama, Yahiko Kambayashi, and Shuichi Miyazaki. Local search algorithms for partial MAXSAT. In Proceedings of AAAI 1997, pages 263-268, 1997. Google Scholar
  16. Mohamed Sami Cherif, Djamal Habet, and André Abramé. Understanding the power of max-sat resolution through up-resilience. Artificial Intelligence, 289:103397, 2020. Google Scholar
  17. Yi Chu, Shaowei Cai, and Chuan Luo. Nuwls-c-2023: Solver description. MaxSAT Evaluation 2023, pages 23-24, 2023. Google Scholar
  18. Yi Chu, Shaowei Cai, and Chuan Luo. Nuwls: Improving local search for (weighted) partial maxsat by new weighting techniques. In Proceedings of AAAI 2023, volume 37, pages 3915-3923, 2023. Google Scholar
  19. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Proceedings of CP 2011, pages 225-239, 2011. Google Scholar
  20. Emir Demirović, Nysret Musliu, and Felix Winter. Modeling and solving staff scheduling with partial weighted maxsat. Annals of Operations Research, 275:79-99, 2019. Google Scholar
  21. Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Proceedings of SAT 2006, pages 252-265, 2006. Google Scholar
  22. Federico Heras, Javier Larrosa, and Albert Oliveras. Minimaxsat: An efficient weighted max-sat solver. Journal of Artificial Intelligence Research, 31:1-32, 2008. Google Scholar
  23. Yuejun Jiang, Henry Kautz, and Bart Selman. Solving problems with hard and soft constraints using a stochastic algorithm for max-sat. In 1st International Joint Workshop on Artificial Intelligence and Operations Research, volume 20. Citeseer, 1995. Google Scholar
  24. Saurabh Joshi, Prateek Kumar, Sukrut Rao, and Ruben Martins. Open-WBO-Inc: Approximation strategies for incomplete weighted MaxSAT. Journal on Satisfiability, Boolean Modeling and Computation, 11(1):73-97, 2019. Google Scholar
  25. Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. QMaxSAT: A partial Max-SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 8(1-2):95-100, 2012. Google Scholar
  26. Adrian Kügel. Improved exact solver for the weighted MAX-SAT problem. In POS-10. In Proceedings of Workshop Pragmatics of SAT,, Edinburgh, UK, 2010, volume 8, pages 15-27, 2010. Google Scholar
  27. Javier Larrosa, Federico Heras, and Simon De Givry. A logical approach to efficient max-sat solving. Artificial Intelligence, 172(2-3):204-233, 2008. Google Scholar
  28. Zhendong Lei and Shaowei Cai. Solving (weighted) partial MaxSAT by dynamic local search for SAT. In Proceedings of IJCAI 2018, pages 1346-1352, 2018. Google Scholar
  29. Zhendong Lei, Shaowei Cai, Fei Geng, Dongxu Wang, Yongrong Peng, Dongdong Wan, Yiping Deng, and Pinyan Lu. Satlike-c: Solver description. MaxSAT Evaluation, 2021:19-20, 2021. Google Scholar
  30. Chu Min Li and Felip Manyà. Maxsat, hard and soft constraints. In Handbook of satisfiability, pages 903-927. IOS Press, 2021. Google Scholar
  31. Chu Min Li, Felip Manya, and Jordi Planes. New inference rules for max-sat. Journal of Artificial Intelligence Research, 30:321-359, 2007. Google Scholar
  32. Chu Min Li and Zhe Quan. An efficient branch-and-bound algorithm based on maxsat for the maximum clique problem. In Proceedings of AAAI 2010, pages 128-133, 2010. URL: https://doi.org/10.1609/AAAI.V24I1.7536.
  33. Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining clause learning and branch and bound for maxsat. In Proceedings of CP 2021, pages 38:1-38:18, 2021. URL: https://doi.org/10.4230/LIPICS.CP.2021.38.
  34. Chuan Luo, Shaowei Cai, Kaile Su, and Wenxuan Huang. CCEHC: An efficient local search algorithm for weighted partial maximum satisfiability. Artificial Intelligence, 243:26-44, 2017. Google Scholar
  35. Ruben Martins, Saurabh Joshi, Vasco Manquinho, and Inês Lynce. Incremental cardinality constraints for MaxSAT. In Proceedings of CP 2014, pages 531-548, 2014. Google Scholar
  36. Ruben Martins, Vasco Manquinho, and Inês Lynce. Open-WBO: A modular maxsat solver. In Proceedings of SAT 2014, pages 438-445, 2014. Google Scholar
  37. Alexander Nadel. Solving maxsat with bit-vector optimization. In Proceedings of SAT 2018, pages 54-72. Springer, 2018. Google Scholar
  38. Alexander Nadel. Anytime weighted MaxSAT with improved polarity selection and bit-vector optimization. In Proceedings of FMCAD 2019, pages 193-202, 2019. Google Scholar
  39. Alexander Nadel. On optimizing a generic function in SAT. In Proceedings of FMCAD 2020, pages 205-213, 2020. Google Scholar
  40. Alexander Nadel. Polarity and variable selection heuristics for sat-based anytime maxsat. Journal on Satisfiability, Boolean Modeling and Computation, 12(1):17-22, 2020. Google Scholar
  41. Alexander Nadel. TT-Open-WBO-Inc-20: an anytime MaxSAT solver entering MSE’20. In Proceedings of MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, pages 21-22, 2020. Google Scholar
  42. Alexander Nadel. Introducing intel (r) sat solver. In Proceedings of SAT 2022, pages 8:1-8:23, 2022. Google Scholar
  43. Alexander Nadel. Tt-open-wbo-inc-23: an anytime maxsat solver entering mse’23. MaxSAT Evaluation 2023, page 29, 2023. Google Scholar
  44. Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. In Proceedings of AAAI 2014, pages 2717-2723, 2014. Google Scholar
  45. John Thornton, Stuart Bain, Abdul Sattar, and Duc Nghia Pham. A two level local search for MAX-SAT problems with hard and soft constraints. In Proceedings of AI 2002, pages 603-614, 2002. Google Scholar
  46. John Thornton and Abdul Sattar. Dynamic constraint weighting for over-constrained problems. In Proceedings of PRICAI 1998, pages 377-388, 1998. Google Scholar
  47. Furong Ye, Chuan Luo, and Shaowei Cai. Better understandings and configurations in maxsat local search solvers via anytime performance analysis. arXiv preprint, 2024. URL: https://arxiv.org/abs/2403.06568.
  48. Jiongzhi Zheng, Kun He, Mingming Jin, Zhuo Chen, and Jinghui Xue. Combining bandmaxsat and fps with nuwls-c. MaxSAT Evaluation 2023, pages 25-26, 2023. Google Scholar
  49. Jiongzhi Zheng, Kun He, and Jianrong Zhou. Farsighted Probabilistic Sampling based local search for (weighted) partial maxsat. In Proceedings of AAAI 2023, pages 4132-4139, 2023. Google Scholar
  50. Jiongzhi Zheng, Kun He, Jianrong Zhou, Yan Jin, Chu-Min Li, and Felip Manya. BandMaxSAT: A local search maxsat solver with multi-armed bandit. In Proceedings of IJCAI 2022, pages 1901-1907, 2022. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact