Document Open Access Logo

Enhanced Lower Bound Computation in Branch-and-Bound for MaxSAT

Authors Jialu Zhang , Chu-Min Li , Sami Cherif , Shuolin Li

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.60.pdf
  • Filesize: 1 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • Maximum Satisfiability
  • Branch and Bound
  • Lower Bound

Metrics

Abstract

Maximum Satisfiability (MaxSAT) is an optimization extension of the Satisfiability (SAT) problem. In Branch-and-Bound (BnB) MaxSAT solving, the quality of the lower bound estimation is critical for effective search space pruning. State-of-the-art BnB solvers typically estimate this bound by identifying disjoint inconsistent subformulas (cores) via Unit Propagation (UP). However, a limitation of this standard approach is that UP fails to detect cores that exhibit complex dependencies with already identified cores. In this paper, we propose a further lookahead algorithm that leverages pre-detected cores to uncover additional disjoint inconsistencies, thereby tightening the lower bound. Experimental results demonstrate that the proposed algorithm significantly tightens the lower bound, enabling the state of the art BnB solver MaxCDCL to solve more instances.

Cite As Get BibTex

Jialu Zhang, Chu-Min Li, Sami Cherif, and Shuolin Li. Enhanced Lower Bound Computation in Branch-and-Bound for MaxSAT. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 60:1-60:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.60

Author Details

Jialu Zhang
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Chu-Min Li
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Sami Cherif
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Shuolin Li
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France

Funding

This work is partially supported by the Chair ANR-19-CHIA-0013-01 (MASSAL’IA), co-funded by the electricity distribution network operator Enedis, as well as by the project ANR-24-CE23-6126 (BforSAT). It was granted access to HPC resources of "Plateforme MatriCS" within University of Picardie Jules Verne, co-funded by the European Union with the European Regional Development Fund (FEDER) and the Hauts-De-France Regional Council.

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., pages 89-128, 2014. URL: https://doi.org/10.3233/SAT190104.
  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. URL: https://doi.org/10.1016/J.ARTINT.2014.03.005.
  3. Carlos Ansótegui, Maria Bonet, Jordi Levy, and Chu-Min Li. Analysis and generation of pseudo-industrial maxsat instances. Frontiers in Artificial Intelligence and Applications, 248:173-184, January 2012. URL: https://doi.org/10.3233/978-1-61499-139-7-173.
  4. Florent Avellaneda. Evalmaxsat 2024. MaxSAT Evaluation 2024 Solver and Benchmark Descriptions, page 8, 2024. Google Scholar
  5. Fahiem Bacchus. Maxhs in the 2020 maxsat evaluation. MaxSAT Evaluation 2020 Solver and Benchmark Descriptions, pages 19-20, 2020. Google Scholar
  6. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pages 929-991. IOS PRESS, Netherlands, 2 edition, 2021. URL: https://doi.org/10.3233/FAIA201008.
  7. 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. URL: https://doi.org/10.1007/978-3-031-38499-8_1.
  8. Daniel Berre and Anne Parrain. The sat4j library, release 2.2. JSAT, 7:59-64, January 2010. Google Scholar
  9. María Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for max-sat. Artificial Intelligence, 171(8):606-618, 2007. URL: https://doi.org/10.1016/j.artint.2007.03.001.
  10. Yibin Chen, Sean Safarpour, Joao Marques-Silva, and Andreas Veneris. Automated design debugging with maximum satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 29(11):1804-1817, 2010. URL: https://doi.org/10.1109/TCAD.2010.2061270.
  11. Mohamed Sami Cherif, Djamal Habet, and André Abramé. Understanding the power of max-sat resolution through up-resilience. Artificial Intelligence, 289:103397, 2020. URL: https://doi.org/10.1016/j.artint.2020.103397.
  12. Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux Devendeville. Minimizing working-group conflicts in conference session scheduling through maximum satisfiability. In Paul Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, September 2-6, 2024, Girona, Spain, volume 307 of LIPIcs, pages 34:1-34:11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CP.2024.34.
  13. Jordi Coll, Chu-Min Li, Shuolin Li, Djamal Habet, and Felip Manyà. Solving weighted maximum satisfiability with branch and bound and clause learning. Computers & Operations Research, 183:107195, 2025. URL: https://doi.org/10.1016/j.cor.2025.107195.
  14. Emir Demirović and Nysret Musliu. Maxsat-based large neighborhood search for high school timetabling. Computers & Operations Research, 78:172-180, 2017. URL: https://doi.org/10.1016/j.cor.2016.08.004.
  15. Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Proceedings of SAT 2006, pages 252-265, 2006. URL: https://doi.org/10.1007/11814948_25.
  16. Federico Heras, Javier Larrosa, and Albert Oliveras. MiniMaxSAT: An efficient Weighted Max-SAT solver. Journal of Artificial Intelligence Research, pages 1-32, 2008. URL: https://doi.org/10.1613/JAIR.2347.
  17. Hao Hu, Marie-José Huguet, and Mohamed Siala. Optimizing Binary Decision Diagrams with MaxSAT for Classification. In 36th AAAI Conference on Artificial Intelligence, Vancouver, Canada, February 2022. Google Scholar
  18. Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown, and Thomas Stützle. Paramils: an automatic algorithm configuration framework. J. Artif. Int. Res., 36(1):267-306, September 2009. URL: https://doi.org/10.1613/JAIR.2861.
  19. Alexey Ignatiev and Joao Marques-Silva. Xai-mindset2: Explainable ai with maxsat. MaxSAT Evaluation 2018: Solver and Benchmark Descriptions, page 43, 2018. Google Scholar
  20. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. RC2: an Efficient MaxSAT Solver. Journal on Satisfiability, Boolean Modeling and Computation, 11(1):53-64, September 2019. URL: https://doi.org/10.3233/SAT190116.
  21. Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. QMaxSAT: A partial Max-SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, pages 95-100, 2012. URL: https://doi.org/10.3233/SAT190091.
  22. 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
  23. Chu Min Li, Shuolin Li, Jordi Coll, Djamal Habet, Felip Manyà, and Kun He. Maxcdcl in maxsat evaluation 2024. MaxSAT Evaluation 2024 Solver and Benchmark Descriptions, pages 15-16, 2024. Google Scholar
  24. Chu Min Li and Felip Manyà. Chapter 23. MaxSAT, Hard and Soft Constraints. In Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications. IOS Press, February 2021. URL: https://doi.org/10.3233/FAIA201007.
  25. Chu-Min Li, Felip Manyà, and Jordi Planes. Detecting disjoint inconsistent subformulas for computing lower bounds for max-sat. In Proceedings of the 21st National Conference on Artificial Intelligence - Volume 1, AAAI'06, pages 86-91. AAAI Press, 2006. URL: http://www.aaai.org/Library/AAAI/2006/aaai06-014.php.
  26. Chu Min Li, Felip Manyà, and Jordi Planes. New inference rules for Max-SAT. Journal of Artificial Intelligence Research, pages 321-359, 2007. URL: https://doi.org/10.1613/JAIR.2215.
  27. Chu-Min Li, Felip Manya, and JR Soler. A clause tableau calculus for maxsat. In IJCAI International Joint Conference on Artificial Intelligence, volume 2016, pages 766-772. International Joint Conferences on Artificial Intelligence, 2016. Google Scholar
  28. 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.
  29. Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining Clause Learning and Branch and Bound for MaxSAT. In Laurent D. Michel, editor, CP 2021, volume 210 of LIPIcs, pages 38:1-38:18, Dagstuhl, Germany, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.38.
  30. Shuolin Li, Chu-Min Li, Jordi Coll, Djamal Habet, and Felip Manyà. Improving the lower bound in branch-and-bound algorithms for maxsat. In Proceedings of the AAAI Conference on Artificial Intelligence, AAAI'25/IAAI'25/EAAI'25. AAAI Press, 2025. URL: https://doi.org/10.1609/aaai.v39i11.33226.
  31. Shuolin Li, Chu Min Li, Jordi Coll, Djamal Habet, Felip Manyà, and Kun He. Wmaxcdcl in maxsat evaluation 2024. MaxSAT Evaluation 2024 Solver and Benchmark Descriptions, pages 17-18, 2024. Google Scholar
  32. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Open-WBO: A modular MaxSAT solver. In Proceedings of SAT 2014, pages 438-445, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_33.
  33. Shiwei Pan, Yiyuan Wang, and Shaowei Cai. An efficient core-guided solver for weighted partial maxsat. In James Kwok, editor, IJCAI-25, pages 2647-2656. International Joint Conferences on Artificial Intelligence Organization, August 2025. Main Track. URL: https://doi.org/10.24963/ijcai.2025/295.
  34. Shiwei Pan, Yiyuan Wang, Shaowei Cai, Jiangnan Li, Wenbo Zhu, and Minghao Yin. Cashwmaxsat-disjcad: Solver description. MaxSAT Evaluation 2024 Solver and Benchmark Descriptions, page 25, 2024. Google Scholar
  35. Tobias Paxian and Bernd Becker. Pacose: An iterative sat-based maxsat solver. MaxSAT Evaluation 2024 Solver and Benchmark Descriptions, page 26, 2024. Google Scholar
  36. Marek Piotrów. Uwrmaxsat: Efficient solver for maxsat and pseudo-boolean problems. In 2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI), pages 132-136, 2020. URL: https://doi.org/10.1109/ICTAI50040.2020.00031.
  37. Marek Piotrów. Uwrmaxsat entering the maxsat evaluation 2024. MaxSAT Evaluation 2024 Solver and Benchmark Descriptions, pages 27-28, 2024. Google Scholar
  38. Sean Safarpour, Hratch Mangassarian, Andreas Veneris, Mark H. Liffiton, and Karem A. Sakallah. Improved design debugging using maximum satisfiability. In Formal Methods in Computer Aided Design (FMCAD'07), pages 13-19, 2007. URL: https://doi.org/10.1109/FAMCAD.2007.26.
  39. Paul Saikko, Jeremias Berg, and Matti Järvisalo. LMHS: A SAT-IP hybrid MaxSAT solver. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016, pages 539-546, Cham, 2016. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-40970-2_34.
  40. Richard J. Wallace and Eugene C. Freuder. Comparative studies of constraint satisfaction and davis-putnam algorithms for maximum satisfiability problems. In David S. Johnson and Michael A. Trick, editors, Cliques, Coloring, and Satisfiability, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, October 11-13, 1993, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 587-615. DIMACS/AMS, 1993. URL: https://doi.org/10.1090/DIMACS/026/28.
  41. Christopher J. C. H. Watkins and Peter Dayan. Technical note: Q-learning. Mach. Learn., 8(3–4):279-292, May 1992. URL: https://doi.org/10.1007/BF00992698.
  42. Zhifei Zheng, Sami Cherif, and Rui Sá Shibasaki. Optimizing power peaks in simple assembly line balancing through maximum satisfiability. In 36th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2024, Herndon, VA, USA, October 28-30, 2024, pages 363-370. IEEE, 2024. URL: https://doi.org/10.1109/ICTAI62512.2024.00060.
  43. Zhaoyang Zhou, Chu-Min Li, Chong Huang, and Ruchu Xu. An exact algorithm with learning for the graph coloring problem. Computers & operations research, 51:282-301, 2014. URL: https://doi.org/10.1016/J.COR.2014.05.017.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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