{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,26]],"date-time":"2026-10-26T06:02:16Z","timestamp":1792994536456,"version":"4.5.0"},"reference-count":58,"publisher":"SAGE Publications","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2022,7,18]]},"abstract":"<jats:p>The Maximum Satisfiability Problem, or MaxSAT, offers a suitable problem solving formalism for combinatorial optimization problems. Nevertheless, MaxSAT solvers implementing the Branch-and-Bound (BnB) scheme have not succeeded in solving challenging real-world optimization problems. It is widely believed that BnB MaxSAT solvers are only superior on random and some specific crafted instances. At the same time, SAT-based MaxSAT solvers perform particularly well on real-world instances. To overcome this shortcoming of BnB MaxSAT solvers, this paper proposes a new BnB MaxSAT solver called MaxCDCL. The main feature of MaxCDCL is the combination of clause learning of soft conflicts and an efficient bounding procedure. Moreover, the paper reports on an experimental investigation showing that MaxCDCL is competitive when compared with the best performing solvers of the 2020 MaxSAT Evaluation. MaxCDCL performs very well on real-world instances, and solves a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best performing MaxSAT solvers, solves the highest number of instances of a collection from all the MaxSAT evaluations held so far.<\/jats:p>","DOI":"10.3233\/aic-210178","type":"journal-article","created":{"date-parts":[[2021,12,24]],"date-time":"2021-12-24T10:25:44Z","timestamp":1640341544000},"page":"131-151","source":"Crossref","is-referenced-by-count":14,"title":["Boosting branch-and-bound MaxSAT solvers with clause learning"],"prefix":"10.1177","volume":"35","author":[{"given":"Chu-Min","family":"Li","sequence":"first","affiliation":[{"name":"Huazhong University of Science and Technology, Wuhan, China"},{"name":"Universit\u00e9 de Picardie Jules Verne, Amiens, France"},{"name":"Aix Marseille Univ, Universit\u00e9 de Toulon, CNRS, LIS, Marseille, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhenxing","family":"Xu","sequence":"additional","affiliation":[{"name":"Huazhong University of Science and Technology, Wuhan, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jordi","family":"Coll","sequence":"additional","affiliation":[{"name":"Aix Marseille Univ, Universit\u00e9 de Toulon, CNRS, LIS, Marseille, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Felip","family":"Many\u00e0","sequence":"additional","affiliation":[{"name":"Artificial Intelligence Research Institute, CSIC, Bellaterra, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Djamal","family":"Habet","sequence":"additional","affiliation":[{"name":"Aix Marseille Univ, Universit\u00e9 de Toulon, CNRS, LIS, Marseille, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kun","family":"He","sequence":"additional","affiliation":[{"name":"Huazhong University of Science and Technology, Wuhan, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"179","reference":[{"key":"10.3233\/AIC-210178_ref1","first-page":"89","article-title":"Description and evaluation of a branch and bound Max-SAT solver","volume":"9","author":"Abram\u00e9","year":"2014","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"10.3233\/AIC-210178_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10428-7_10"},{"key":"10.3233\/AIC-210178_ref3","doi-asserted-by":"crossref","unstructured":"A. Abram\u00e9 and D. Habet, Learning nobetter clauses in Max-SAT branch and bound solvers, in: Proceedings of ICTAI 2016, 2016, pp. 452\u2013459.","DOI":"10.1109\/ICTAI.2016.0075"},{"key":"10.3233\/AIC-210178_ref4","unstructured":"T. Alsinet, F. Many\u00e0 and J. Planes, Improved branch and bound algorithms for Max-SAT, in: Proceedings of the 6th International Conference on the Theory and Applications of Satisfiability Testing, 2003."},{"key":"10.3233\/AIC-210178_ref5","doi-asserted-by":"crossref","unstructured":"T. Alsinet, F. Many\u00e0 and J. Planes, Improved exact solver for weighted Max-SAT, in: Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing, SAT-2005, St. Andrews, Scotland, LNCS, Vol. 3569, Springer, 2005, pp. 371\u2013377.","DOI":"10.1007\/11499107_27"},{"key":"10.3233\/AIC-210178_ref6","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10898-007-9166-9","article-title":"An efficient solver for weighted Max-SAT","volume":"41","author":"Alsinet","year":"2008","journal-title":"Journal of Global Optimization"},{"key":"10.3233\/AIC-210178_ref7","doi-asserted-by":"crossref","unstructured":"C. Ans\u00f3tegui, M.L. Bonet and J. Levy, Solving (weighted) partial MaxSAT through satisfiability testing, in: Proceedings of SAT 2009, LNCS, Vol. 5584, Springer, 2009, pp. 427\u2013440.","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"10.3233\/AIC-210178_ref8","doi-asserted-by":"crossref","unstructured":"C. Ans\u00f3tegui, M.L. Bonet and J. Levy, A new algorithm for weighted partial MaxSAT, in: Proceedings AAAI 2010, 2010, pp. 3\u20138.","DOI":"10.1609\/aaai.v24i1.7545"},{"key":"10.3233\/AIC-210178_ref9","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.artint.2013.01.002","article-title":"SAT-based MaxSAT algorithms","volume":"196","author":"Ans\u00f3tegui","year":"2013","journal-title":"Artificial Intelligence"},{"key":"10.3233\/AIC-210178_ref10","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.artint.2017.05.003","article-title":"WPM3: An (in)complete algorithm for weighted partial MaxSAT","volume":"250","author":"Ans\u00f3tegui","year":"2017","journal-title":"Artificial Intelligence"},{"key":"10.3233\/AIC-210178_ref11","unstructured":"G. Audemard and L. Simon, Predicting learnt clauses quality in modern SAT solvers, in: Proceedings IJCAI 2009, 2009, pp. 399\u2013404."},{"key":"10.3233\/AIC-210178_ref12","unstructured":"F. Bacchus, MaxHS in the 2020 MaxSAT evaluation, in: MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, 2020, pp. 19\u201320."},{"key":"10.3233\/AIC-210178_ref13","unstructured":"F. Bacchus, J. Berg, M. J\u00e4rvisalo and R. Martins, MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, 2020."},{"key":"10.3233\/AIC-210178_ref14","doi-asserted-by":"crossref","unstructured":"F. Bacchus, A. Hyttinen, M. J\u00e4rvisalo and P. Saikko, Reduced cost fixing in MaxSAT, in: Proceedings of CP 2017, LNCS, Springer, 2017, pp. 641\u2013651.","DOI":"10.1007\/978-3-319-66158-2_41"},{"key":"10.3233\/AIC-210178_ref15","doi-asserted-by":"crossref","unstructured":"F. Bacchus, M. J\u00e4rvisalo and M. Ruben, Maximum satisfiability, in: Handbook of Satisfiability, 2nd edn, IOS Press, 2021, pp. 929\u2013991.","DOI":"10.3233\/FAIA201008"},{"key":"10.3233\/AIC-210178_ref16","doi-asserted-by":"crossref","unstructured":"N. Bansal and V. Raman, Upper bounds for MaxSat: Further improved, in: Proc 10th International Symposium on Algorithms and Computation, ISAAC\u201999, LNCS, Vol. 1741, Springer, Chennai, India, 1999, pp. 247\u2013260.","DOI":"10.1007\/3-540-46632-0_26"},{"key":"10.3233\/AIC-210178_ref17","unstructured":"A. Biere, K. Fazekas, M. Fleury and M. Heisinger, CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020, in: Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, 2020, p. 50."},{"key":"10.3233\/AIC-210178_ref18","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1023\/A:1009725216438","article-title":"A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems","volume":"2","author":"Borchers","year":"1999","journal-title":"Journal of Combinatorial Optimization"},{"key":"10.3233\/AIC-210178_ref19","doi-asserted-by":"crossref","unstructured":"S. Carsten, Towards an optimal CNF encoding of Boolean cardinality constraints, in: Proceedings of CP 2005, LNCS, Vol. 3709, Springer, 2005, pp. 827\u2013831.","DOI":"10.1007\/11564751_73"},{"key":"10.3233\/AIC-210178_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103397"},{"key":"10.3233\/AIC-210178_ref21","doi-asserted-by":"crossref","unstructured":"J. Davies and F. Bacchus, Solving MAXSAT by solving a sequence of simpler SAT instances, in: Proceedings of CP 2011, Springer, 2011, pp. 225\u2013239.","DOI":"10.1007\/978-3-642-23786-7_19"},{"key":"10.3233\/AIC-210178_ref22","doi-asserted-by":"crossref","unstructured":"J. Davies and F. Bacchus, Exploiting the power of MIP solvers in MAXSAT, in: Proceedings of SAT 2013, Springer, 2013, pp. 166\u2013181.","DOI":"10.1007\/978-3-642-39071-5_13"},{"key":"10.3233\/AIC-210178_ref23","doi-asserted-by":"crossref","unstructured":"N. Feng and F. Bacchus, Clause size reduction with all-uip learning, in: Proceedings of SAT 2020, Springer LNCS, Vol. 12178, 2020, pp. 28\u201345.","DOI":"10.1007\/978-3-030-51825-7_3"},{"key":"10.3233\/AIC-210178_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_25"},{"key":"10.3233\/AIC-210178_ref25","doi-asserted-by":"crossref","unstructured":"G. Gange, J. Berg, E. Demirovi\u0107 and P.J. Stuckey, Core-guided and core-boosted search for CP, in: Proceedings of CPAIOR 2020, 2020, pp. 205\u2013221.","DOI":"10.1007\/978-3-030-58942-4_14"},{"key":"10.3233\/AIC-210178_ref26","unstructured":"F. Heras and J. Larrosa, New inference rules for efficient Max-SAT solving, in: Proceedings of the National Conference on Artificial Intelligence, AAAI-2006, Boston\/MA, USA, 2006, pp. 68\u201373."},{"key":"10.3233\/AIC-210178_ref27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1613\/jair.2347","article-title":"MiniMaxSAT: An efficient weighted Max-SAT solver","volume":"31","author":"Heras","year":"2008","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"1","key":"10.3233\/AIC-210178_ref28","first-page":"53","article-title":"RC2: An efficient maxsat solver","volume":"11","author":"Ignatiev","year":"2019","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"1\/2","key":"10.3233\/AIC-210178_ref29","first-page":"95","article-title":"QMaxSAT: A partial Max-SAT solver","volume":"8","author":"Koshimura","year":"2012","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"10.3233\/AIC-210178_ref30","doi-asserted-by":"crossref","unstructured":"A. Kuegel, Improved exact solver for the weighted MAX-SAT problem, in: Proceedings of Workshop Pragmatics of SAT, POS-10, Edinburgh, UK, 2010, pp. 15\u201327.","DOI":"10.29007\/38lm"},{"issue":"2\u20133","key":"10.3233\/AIC-210178_ref31","first-page":"59","article-title":"The Sat4j library, release 2.2","volume":"7","author":"Le Berre","year":"2010","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"10.3233\/AIC-210178_ref32","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/187"},{"key":"10.3233\/AIC-210178_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2019.103197"},{"key":"10.3233\/AIC-210178_ref34","unstructured":"C.-M. Li, Z. Xu, J. Coll, F. Many\u00e0, D. Habet and K. He, Combining clause learning and branch and bound for MaxSAT, in: Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming, CP, Montpellier, France (Virtual Conference), LIPIcs, Vol. 210, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2021, pp. 38:1\u201338:18."},{"key":"10.3233\/AIC-210178_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_43"},{"issue":"4","key":"10.3233\/AIC-210178_ref36","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/s10601-010-9097-9","article-title":"Resolution-based lower bounds in MaxSAT","volume":"15","author":"Li","year":"2010","journal-title":"Constraints"},{"key":"10.3233\/AIC-210178_ref37","unstructured":"C.M. Li and F. Many\u00e0, MaxSAT, hard and soft constraints, in: Handbook of Satisfiability, 2nd edn, IOS Press, 2021, pp. 903\u2013927."},{"key":"10.3233\/AIC-210178_ref38","doi-asserted-by":"crossref","unstructured":"C.M. Li, F. Many\u00e0 and J. Planes, Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers, in: Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming, CP-2005, LNCS, Vol. 3709, Springer, Sitges, Spain, 2005, pp. 403\u2013414.","DOI":"10.1007\/11564751_31"},{"key":"10.3233\/AIC-210178_ref39","unstructured":"C.M. Li, F. Many\u00e0 and J. Planes, Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT, in: Proceedings of the 21st National Conference on Artificial Intelligence, AAAI-2006, Boston\/MA, USA, 2006, pp. 86\u201391."},{"key":"10.3233\/AIC-210178_ref40","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1613\/jair.2215","article-title":"New inference rules for Max-SAT","volume":"30","author":"Li","year":"2007","journal-title":"Journal of Artificial Intelligence Research"},{"key":"10.3233\/AIC-210178_ref41","unstructured":"J.H. Liang, C. Oh, V. Ganesh, K. Czarnecki and P. Poupart, MapleCOMSPS, MapleCOMSPS LRB, MapleCOMSPS CHB, in: Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, 2016, pp. 52\u201353."},{"issue":"4","key":"10.3233\/AIC-210178_ref42","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","article-title":"Optimal speedup of Las Vegas algorithms","volume":"47","author":"Luby","year":"1993","journal-title":"Information Processing Letters"},{"key":"10.3233\/AIC-210178_ref43","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/98"},{"key":"10.3233\/AIC-210178_ref44","doi-asserted-by":"crossref","unstructured":"V.M. Manquinho, J. Marques-Silva and J. Planes, Algorithms for weighted Boolean optimization, in: Proceedings of SAT 2009, LNCS, Vol. 5584, Springer, 2009, pp. 495\u2013508.","DOI":"10.1007\/978-3-642-02777-2_45"},{"key":"10.3233\/AIC-210178_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_24"},{"issue":"8\u20139","key":"10.3233\/AIC-210178_ref46","first-page":"240","volume":"171","author":"Mar\u00eda","year":"2007","journal-title":"Resolution for Max-SAT. Artificial Intelligence"},{"key":"10.3233\/AIC-210178_ref47","doi-asserted-by":"crossref","unstructured":"J. Marques-Silva and V.M. Manquinho, Towards more effective unsatisfiability-based maximum satisfiability algorithms, in: Proceedings of SAT 2008, LNCS, Vol. 4996, Springer, 2008, pp. 225\u2013230.","DOI":"10.1007\/978-3-540-79719-7_21"},{"key":"10.3233\/AIC-210178_ref48","doi-asserted-by":"crossref","unstructured":"R. Martins, V.M. Manquinho and I. Lynce, Open-WBO: A modular MaxSAT solver, in: Proceedings of SAT 2014, LNCS, Vol. 8561, Springer, 2014, pp. 438\u2013445.","DOI":"10.1007\/978-3-319-09284-3_33"},{"key":"10.3233\/AIC-210178_ref49","doi-asserted-by":"crossref","unstructured":"M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang and S.M. Chaff, Engineering an efficient SAT solver, in: Proceedings of DAC 2001, ACM, 2001, pp. 530\u2013535.","DOI":"10.1145\/378239.379017"},{"key":"10.3233\/AIC-210178_ref50","doi-asserted-by":"crossref","unstructured":"N. Narodytska and F. Bacchus, Maximum satisfiability using core-guided MaxSAT resolution, in: Proceedings of AAAI 2014, 2014, pp. 2717\u20132723.","DOI":"10.1609\/aaai.v28i1.9124"},{"key":"10.3233\/AIC-210178_ref51","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1006\/jagm.2000.1075","article-title":"New upper bounds for maximum satisfiability","volume":"36","author":"Niedermeier","year":"2000","journal-title":"Journal of Algorithms"},{"key":"10.3233\/AIC-210178_ref52","unstructured":"T. Paxian and B. Becker, Pacose: An iterative SAT-based MaxSAT solver, in: MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, 2020, p. 12."},{"key":"10.3233\/AIC-210178_ref53","doi-asserted-by":"crossref","unstructured":"P. Saikko, J. Berg and M. J\u00e4rvisalo, LMHS: A SAT-IP hybrid MaxSAT solver, in: Proceedings of SAT 2016, LNCS, Vol. 9710, 2016, pp. 539\u2013546.","DOI":"10.1007\/978-3-319-40970-2_34"},{"key":"10.3233\/AIC-210178_ref54","unstructured":"H. Shen and H. Zhang, Study of lower bound functions for MAX-2-SAT, in: Proceedings of the 19th National Conference on Artificial Intelligence, AAAI-2004, San Jose\/CA, USA, 2004, pp. 185\u2013190."},{"key":"10.3233\/AIC-210178_ref55","doi-asserted-by":"crossref","unstructured":"K. Stepan, Improving implementation of SAT competitions 2017\u20132019 winners, in: Proceedings of SAT 2020, LNCS, Vol. 12178, 2020, pp. 139\u2013148.","DOI":"10.1007\/978-3-030-51825-7_11"},{"key":"10.3233\/AIC-210178_ref56","doi-asserted-by":"crossref","unstructured":"F. Tr\u00f6sser, S. De Givry and G. Katsirelos, Relaxation-aware heuristics for exact optimization in graphical models, in: Prodeedings of CPAIOR 2020, Springer, 2020, pp. 475\u2013491.","DOI":"10.1007\/978-3-030-58942-4_31"},{"issue":"2","key":"10.3233\/AIC-210178_ref57","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.artint.2005.01.004","article-title":"An efficient exact algorithm for (weighted) maximum satisfiability","volume":"164","author":"Xing","year":"2005","journal-title":"Artificial Intelligence"},{"key":"10.3233\/AIC-210178_ref58","unstructured":"A. Zha, QMaxSAT in MaxSAT evaluation 2018, in: Proceedings of the MaxSAT Evaluation 2020, 2020, p. 16."}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-210178","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T18:28:01Z","timestamp":1777400881000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-210178"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,18]]},"references-count":58,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.3233\/aic-210178","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"value":"1875-8452","type":"electronic"},{"value":"0921-7126","type":"print"}],"subject":[],"published":{"date-parts":[[2022,7,18]]}}}