Document Open Access Logo

Beyond Core-Guided MaxSAT

Authors Ilario Bonacina , Jordi Levy , Ion Mikel Liberal

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.9.pdf
  • Filesize: 1.13 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Mathematics of computing → Solvers
Keywords
  • MaxSAT
  • Proof Systems
  • Solvers
  • Optimization

Metrics

Abstract

Several proof systems for MaxSAT have been proposed in the literature, including MaxSAT resolution and, more recently, systems based on polynomial calculus and tableaux. Although these systems are sound and complete and have varying strengths, they fail to capture the specific inferential strategies used by practical MaxSAT solvers, particularly those used in core-guided approaches. As a result, a formula that is hard to prove in these proof systems may not be hard for a solver, and vice versa.
In this paper, we describe a new proof system for MaxSAT, the Comparator Calculus (CC), which models the inferential strategies used in core-guided MaxSAT solvers. Inspired by this formalism, we introduce two new MaxSAT algorithms: a core-guided one (CSimple) and one non-core-guided (CSat), which uses heuristics to construct new soft formulas and calls a SAT solver on a single soft formula. We also define a hybrid mechanism (core-guided CSat) that uses cores to guide the heuristics. 
We evaluate and compare our solvers with OLL on instances from the MaxSAT evaluation 2024, random 2-CNFs, and PHP formulas. Experimental results suggest that, in general, the performance of the different MaxSAT solvers depends on the structure of the instances. On the set of industrial instances of the MaxSAT Evaluation 2024, CSimple performs better than the others (including OLL).

Cite As Get BibTex

Ilario Bonacina, Jordi Levy, and Ion Mikel Liberal. Beyond Core-Guided MaxSAT. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.9

Author Details

Ilario Bonacina
  • Universitat Politècnica de Catalunya, Barcelona, Spain
Jordi Levy
  • IIIA, CSIC, Barcelona, Spain
Ion Mikel Liberal
  • IIIA, CSIC, Barcelona, Spain

Funding

  • Bonacina, Ilario: Funded by the AEI with the grant number PID2022-138506NB-C22.
  • Levy, Jordi: Funded by the AEI with the grant number PID2022-138506NB-C21.
  • Liberal, Ion Mikel: Funded by the AEI with the grant number PID2022-138506NB-C21.

Supplementary Materials

References

  1. Miklós Ajtai, János Komlós, and Endre Szemerédi. An O(n log n) sorting network. In Proceedings of the 15th Annual ACM Symposium on Theory of Computing (STOC), pages 1-9, 1983. URL: https://doi.org/10.1145/800061.808726.
  2. Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, and Jordi Levy. Improving WPM2 for (weighted) partial MaxSAT. In 19th International Conference on Principles and Practice of Constraint Programming, CP 2013, volume 8124 of Lecture Notes in Computer Science, pages 117-132. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40627-0_12.
  3. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. Artif. Intell., 196:77-105, 2013. URL: https://doi.org/10.1016/J.ARTINT.2013.01.002.
  4. Carlos Ansótegui, Frédéric Didier, and Joel Gabàs. Exploiting the structure of unsatisfiable cores in MaxSAT. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pages 283-289. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/046.
  5. Carlos Ansótegui and Joel Gabàs. WPM3: an (in)complete algorithm for weighted partial MaxSAT. Artif. Intell., 250:37-57, 2017. URL: https://doi.org/10.1016/J.ARTINT.2017.05.003.
  6. Carlos Ansótegui, Joel Gabàs, and Jordi Levy. Exploiting subproblem optimization in SAT-based MaxSAT algorithms. J. Heuristics, 22(1):1-53, 2016. URL: https://doi.org/10.1007/S10732-015-9300-7.
  7. Carlos Ansótegui, Jesus Ojeda, António Pacheco, Josep Pon, Josep M. Salvia, and Eduard Torres. Optilog: A framework for SAT-based systems. In Proceedings of the 24th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 1-10, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_1.
  8. Josep Argelich, Chu Min Li, Felip Manyà, and Joan Ramon Soler. Clause tableaux for maximum and minimum satisfiability. Log. J. IGPL, 29(1):7-27, 2021. URL: https://doi.org/10.1093/JIGPAL/JZZ025.
  9. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks: a theoretical and empirical study. Constraints An Int. J., 16(2):195-221, 2011. URL: https://doi.org/10.1007/S10601-010-9105-0.
  10. Gilles Audemard and Laurent Simon. On the Glucose SAT solver. Int. J. Artif. Intell. Tools, 27(1):1840001:1-1840001:25, 2018. URL: https://doi.org/10.1142/S0218213018400018.
  11. Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified core-guided MaxSAT solving. In Proceedings of the 29th International Conference on Automated Deduction (CADE), pages 1-22, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_1.
  12. Jeremias Berg, Matti Järvisalo, Ruben Martins, Andreas Niskanen, and Tobias Paxian, editors. MaxSAT Evaluation 2024: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2024. Google Scholar
  13. Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Polynomial calculus for MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, volume 271 of LIPIcs, pages 5:1-5:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.5.
  14. Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Polynomial calculus for optimization. Artif. Intell., 337:104208, 2024. URL: https://doi.org/10.1016/J.ARTINT.2024.104208.
  15. Ilario Bonacina, Jordi Levy, and Ion Mikel Liberal. Beyond Core-Guided MaxSAT. Software, Funded by the AEI with the grant number PID2022-138506NB-C21 and PID2022-138506NB-C22., (visited on 2026-06-30). URL: https://github.com/Equipomaxsat/Beyond-Core-Guided-MaxSAT.git
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26940
  16. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. A complete calculus for Max-SAT. In 9th International Conference on Theory and Applications of Satisfiability Testing - SAT 2006, volume 4121 of Lecture Notes in Computer Science, pages 240-251. Springer, 2006. URL: https://doi.org/10.1007/11814948_24.
  17. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for Max-SAT. Artif. Intell., 171(8-9):606-618, 2007. URL: https://doi.org/10.1016/J.ARTINT.2007.03.001.
  18. Vasek Chvátal and Bruce A. Reed. Mick gets some (the odds are on his side). In Proceedings of the 33rd Annual Symposium on Foundations of Computer Science (FOCS), pages 620-627, 1992. URL: https://doi.org/10.1109/SFCS.1992.267789.
  19. Michael Codish and Moshe Zazon-Ivry. Pairwise cardinality networks. In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pages 154-172, 2010. URL: https://doi.org/10.1007/978-3-642-17511-4_10.
  20. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP), pages 225-239, 2011. URL: https://doi.org/10.1007/978-3-642-23786-7_19.
  21. Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 252-265, 2006. URL: https://doi.org/10.1007/11814948_25.
  22. Andreas Goerdt. A threshold for unsatisfiability. J. Comput. Syst. Sci., 53(3):469-486, 1996. URL: https://doi.org/10.1006/JCSS.1996.0081.
  23. Johan Håstad. On small-depth Frege proofs for PHP. In Proceedings of 2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS), pages 37-49, 2023. URL: https://doi.org/10.1109/FOCS57990.2023.00010.
  24. Johan Håstad. On small-depth Frege proofs for tseitin for grids. J. ACM, 68(1), 2020. URL: https://doi.org/10.1145/3425606.
  25. 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. URL: https://doi.org/10.3233/SAT190116.
  26. Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Unifying core-guided and implicit hitting set based optimization. In Proceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI), pages 1935-1943, 2023. URL: https://doi.org/10.24963/IJCAI.2023/215.
  27. Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, and Jakob Nordström. Certified MaxSAT preprocessing. In Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR), pages 396-418, 2024. URL: https://doi.org/10.1007/978-3-031-63498-7_24.
  28. George Katsirelos. Core-guided linear programming-based maximum satisfiability. In 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025, volume 341 of LIPIcs, pages 17:1-17:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.17.
  29. Jan Krajíček. Proof Complexity. Cambridge University Press, 2019. Google Scholar
  30. Chu Min Li, Felip Manyà, Nouredine Ould Mohamedou, and Jordi Planes. Resolution-based lower bounds in MaxSAT. Constraints An Int. J., 15(4):456-484, 2010. URL: https://doi.org/10.1007/S10601-010-9097-9.
  31. Chu Min Li, Felip Manyà, and Joan Ramon Soler. A clause tableau calculus for MaxSAT. In Subbarao Kambhampati, editor, Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, pages 766-772. IJCAI/AAAI Press, 2016. URL: http://www.ijcai.org/Abstract/16/114.
  32. 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, volume 210 of LIPIcs, pages 38:1-38:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.38.
  33. António Morgado, Carmine Dodaro, and João Marques-Silva. Core-guided MaxSAT with soft cardinality constraints. In Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming (CP), pages 564-573, 2014. URL: https://doi.org/10.1007/978-3-319-10428-7_41.
  34. António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and João Marques-Silva. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints An Int. J., 18(4):478-534, 2013. URL: https://doi.org/10.1007/S10601-013-9146-2.
  35. António Morgado, Alexey Ignatiev, and João Marques-Silva. MSCG: robust core-guided MaxSAT solving. J. Satisf. Boolean Model. Comput., 9(1):129-134, 2014. URL: https://doi.org/10.3233/SAT190105.
  36. Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. In Proceedings of the 28th Conference on Artificial Intelligence (AAAI), pages 2717-2723, 2014. URL: https://doi.org/10.1609/AAAI.V28I1.9124.
  37. Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Incremental Maximum Satisfiability. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), volume 236 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1-14:19, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.14.
  38. Toru Ogawa, Yangyang Liu, Ryuzo Hasegawa, Miyuki Koshimura, and Hiroshi Fujita. Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers. In Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pages 9-17, 2013. URL: https://doi.org/10.1109/ICTAI.2013.13.
  39. Paul Saikko, Jeremias Berg, and Matti Järvisalo. LMHS: a SAT-IP hybrid MaxSAT solver. In Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 539-546, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_34.
  40. André Schidler and Stefan Szeider. Analyzing reformulation performance in core-guided maxsat solving. In 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025, volume 341 of LIPIcs, pages 26:1-26:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.26.
  41. Xujie Si, Xin Zhang, Vasco Manquinho, Mikoláš Janota, Alexey Ignatiev, and Mayur Naik. On incremental core-guided maxsat solving. In Michel Rueher, editor, Principles and Practice of Constraint Programming, pages 473-482, Cham, 2016. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-44953-1_30.
  42. G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus, pages 466-483. Springer Berlin Heidelberg, Berlin, Heidelberg, 1983. URL: https://doi.org/10.1007/978-3-642-81955-1_28.
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