Document Open Access Logo

Combining Clause Learning and Branch and Bound for MaxSAT

Authors Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, Kun He

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.38.pdf
  • Filesize: 0.88 MB
  • 18 pages

Document Identifiers

Author Details

Chu-Min Li
  • Huazhong University of Science and Technology, Wuhan, China
  • Université de Picardie Jules Verne, Amiens, France
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
Zhenxing Xu
  • Huazhong University of Science and Technology, Wuhan, China
Jordi Coll
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
Felip Manyà
  • Artificial Intelligence Research Institute, CSIC, Bellaterra, Spain
Djamal Habet
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
Kun He
  • Huazhong University of Science and Technology, Wuhan, China

Funding

This work has been partially funded by the French Agence Nationale de la Recherche, reference ANR-19-CHIA-0013-01, and the Spanish AEI project PID2019-111544GB-C2.

Acknowledgements

This work has been partially supported by Archimedes Institute, Aix-Marseille University. We thank the anonymous reviewers for their comments and suggestions that helped to improve the manuscript.

Cite AsGet BibTex

Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining Clause Learning and Branch and Bound for MaxSAT. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.38

Abstract

Branch and Bound (BnB) is a powerful technique that has been successfully used to solve many combinatorial optimization problems. However, MaxSAT is a notorious exception because BnB MaxSAT solvers perform poorly on many instances encoding interesting real-world and academic optimization problems. This has formed a prevailing opinion in the community stating that BnB is not so useful for MaxSAT, except for random and some special crafted instances. In fact, there has been no advance allowing to significantly speed up BnB MaxSAT solvers in the past few years, as illustrated by the absence of BnB solvers in the annual MaxSAT Evaluation since 2017. Our work aims to change this situation and proposes a new BnB MaxSAT solver, called MaxCDCL, by combining clause learning and an efficient bounding procedure. The experimental results show that, contrary to the prevailing opinion, BnB can be competitive for MaxSAT. MaxCDCL is ranked among the top 5 solvers of the 15 solvers that participated in the 2020 MaxSAT Evaluation, solving a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best existing solvers, solves the highest number of instances of the MaxSAT Evaluations.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Constraints
Keywords
  • MaxSAT
  • Branch&Bound
  • CDCL

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. J. Satisf. Boolean Model. Comput., 9:89-128, 2014. Google Scholar
  2. André Abramé and Djamal Habet. Learning nobetter clauses in Max-SAT branch and bound solvers. In Proceedings of ICTAI 2016, pages 452-459, 2016. Google Scholar
  3. Carlos Ansótegui, María Luisa Bonet, and Jordi Levy. Solving (Weighted) Partial MaxSAT through satisfiability testing. In Proceedings of SAT 2009, pages 427-440. Springer LNCS 5584, 2009. Google Scholar
  4. Carlos Ansótegui, María Luisa Bonet, and Jordi Levy. A new algorithm for weighted partial MaxSAT. In Proceedings 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. Predicting learnt clauses quality in modern SAT solvers. In Proceedings IJCAI 2009, pages 399-404, 2009. Google Scholar
  8. Fahiem Bacchus. MaxHS in the 2020 MaxSAT Evaluation. In MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, pages 19-20, 2020. Google Scholar
  9. Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins. MaxSAT Evaluation 2020: Solver and benchmark descriptions, 2020. Google Scholar
  10. Fahiem Bacchus, Antti Hyttinen, Matti Järvisalo, and Paul Saikko. Reduced cost fixing in MaxSAT. In Proceedings of CP 2017, Springer LNCS, pages 641-651, 2017. Google Scholar
  11. Fahiem Bacchus, Matti Järvisalo, and Martins Ruben. Maximum satisfiability. In Handbook of satisfiability, second edition, pages 929-991. IOS Press, 2021. Google Scholar
  12. Daniel Le Berre and Anne Parrain. The Sat4j library, release 2.2. J. Satisf. Boolean Model. Comput., 7(2-3):59-6, 2010. Google Scholar
  13. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximilian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, page 50, 2020. Google Scholar
  14. 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
  15. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Proceedings of CP 2011, page 225–239. Springer, 2011. Google Scholar
  16. Jessica Davies and Fahiem Bacchus. Exploiting the power of MIP solvers in MAXSAT. In Proceedings of SAT 2013, pages 166-181. Springer, 2013. Google Scholar
  17. Jo Devriendt, Ambros Gleixner, and Jakob Nordström. Learn to relax: Integrating 0-1 integer linear programming with pseudo-boolean conflict-driven search. Constraints, pages 1-30, 2021. Google Scholar
  18. Nick Feng and Fahiem Bacchus. Clause size reduction with all-uip learning. In Proceedings of SAT 2020, Springer LNCS 12178, pages 28-45, 2020. Google Scholar
  19. Graeme Gange, Jeremias Berg, Emir Demirović, and Peter J Stuckey. Core-guided and core-boosted search for CP. In Proceedings of CPAIOR 2020, pages 205-221, 2020. Google Scholar
  20. 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
  21. Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an efficient maxsat solver. J. Satisf. Boolean Model. Comput., 11(1):53-64, 2019. Google Scholar
  22. Stepan Kochemazov. Improving implementation of SAT competitions 2017–2019 winners. In Proceedings of SAT 2020, LNCS 12178, pages 139-148, 2020. Google Scholar
  23. Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. QMaxSAT: A Partial Max-SAT solver. J. Satisf. Boolean Model. Comput., 8(1/2):95-100, 2012. Google Scholar
  24. Adrian Kuegel. Improved exact solver for the Weighted MAX-SAT problem. In Proceedings of Workshop Pragmatics of SAT, POS-10, Edinburgh, UK, pages 15-27, 2010. Google Scholar
  25. 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
  26. Chu Min Li and Felip Manyà. MaxSAT, hard and soft constraints. In Handbook of satisfiability, second edition, pages 903-927. IOS Press, 2021. Google Scholar
  27. Chu Min Li, Felip Manya, Nouredine Ould Mohamedou, and Jordi Planes. Resolution-based lower bounds in MaxSAT. Constraints, 15(4):456-484, 2010. Google Scholar
  28. Chu Min Li, Felip Manya, and Jordi Planes. Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers. In Proceedings of CP 2005, pages 403-414. Springer, 2005. Google Scholar
  29. Chu Min Li, Felip Manya, and Jordi Planes. Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT. In Proceedings of AAAI 2006, pages 86-91, 2006. Google Scholar
  30. Chu Min Li, Felip Manyà, and Jordi Planes. New inference rules for Max-SAT. Journal of Artificial Intelligence Research, 30:321-359, 2007. Google Scholar
  31. Chu-Min Li, Fan Xiao, Mao Luo, Felip Manyà, Zhipeng Lü, and Yu Li. Clause vivification by unit propagation in CDCL SAT solvers. Artificial Intelligence, 279, 2020. Google Scholar
  32. Jia Hui Liang, Chanseok Oh, Vijay Ganesh, Krzysztof Czarnecki, and Pascal Poupart. MapleCOMSPS, MapleCOMSPS LRB, MapleCOMSPS CHB. In Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, pages 52-53, 2016. Google Scholar
  33. Michael Luby, Alistair Sinclair, and David Zuckerman. Optimal speedup of Las Vegas algorithms. Information Processing Letters, 47(4):173-180, 1993. Google Scholar
  34. Mao Luo, Chu-Min Li, Fan Xiao, Felip Manyà, and Zhipeng Lü. An effective learnt clause minimization approach for CDCL SAT solvers. In Proceedings of IJCAI 2017, pages 703-711, 2017. Google Scholar
  35. Vasco M. Manquinho, Joao Marques-Silva, and Jordi Planes. Algorithms for weighted Boolean optimization. In Proceedings of SAT 2009, pages 495-508. Springer LNCS 5584, 2009. Google Scholar
  36. Joao Marques-Silva and Vasco M. Manquinho. Towards more effective unsatisfiability-based maximum satisfiability algorithms. In Proceedings of SAT 2008, pages 225-230. Springer LNCS 4996, 2008. Google Scholar
  37. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Open-WBO: A modular MaxSAT solver. In Proceedings of SAT 2014, volume 8561 of LNCS, pages 438-445. Springer, 2014. Google Scholar
  38. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of DAC 2001, pages 530-535. ACM, 2001. Google Scholar
  39. Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. In Proceedings of AAAI 2014, pages 2717-2723, 2014. Google Scholar
  40. Tobias Paxian and Bernd Becker. Pacose: An iterative SAT-based MaxSAT solver. In MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, page 12, 2020. Google Scholar
  41. Paul Saikko, Jeremias Berg, and Matti Järvisalo. LMHS: A SAT-IP hybrid MaxSAT solver. In Proceedings of SAT 2016, volume 9710 of LNCS, pages 539-546, 2016. Google Scholar
  42. Carsten Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In Proceedings of CP 2005, pages 827-831. Springer LNCS 3709, 2005. Google Scholar
  43. Fulya Trösser, Simon De Givry, and George Katsirelos. Relaxation-aware heuristics for exact optimization in graphical models. In Prodeedings of CPAIOR 2020, pages 475-491. Springer, 2020. Google Scholar
  44. Aolong Zha. QMaxSAT in MaxSAT Evaluation 2018. In Proceedings of the MaxSAT Evaluation 2020, page 16, 2020. 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 Imprint Privacy Contact