Document Open Access Logo

Hermax: A Unified MaxSAT Library (Tool Paper)

Authors Josep Maria Salvia Hornos , Cèsar Fernández Camón , Carles Mateu Piñol

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.41.pdf
  • Filesize: 0.93 MB
  • 13 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Constraint and logic programming
  • Mathematics of computing → Discrete optimization
  • Software and its engineering → Software libraries and repositories
Keywords
  • MaxSAT
  • Incremental Solving
  • IPAMIR
  • Python
  • Constraint modelling

Metrics

Abstract

Despite the utility of Maximum Satisfiability (MaxSAT) in discrete optimization, developing iterative workflows remains cumbersome due to fragmented, low-level solver APIs. We present Hermax, a unified Python library and modelling compiler for MaxSAT. Hermax provides an IPAMIR interface that exposes incremental solving, assumptions, and weight updates through a single API across many incremental and non-incremental backends. Furthermore, it introduces a compiler with Constraint Programming primitives that translates high-level models directly into optimized CNF/WCNF through eager evaluation. This compiler allows automatic optimizations like integer ladder graph encoding that bypasses Pseudo-Boolean formulation when possible. Together, these features enable rapid prototyping and production grade optimization directly from Python across major platforms and hardware architectures.

Cite As Get BibTex

Josep Maria Salvia Hornos, Cèsar Fernández Camón, and Carles Mateu Piñol. Hermax: A Unified MaxSAT Library (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 41:1-41:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.41

Author Details

Josep Maria Salvia Hornos
  • Department of Computer Engineering and Digital Design, University of Lleida, Spain
  • Department of IT and Systems, AI Division, Corporación Alimentaria Guissona S.A., Lleida, Spain
Cèsar Fernández Camón
  • Department of Computer Engineering and Digital Design, University of Lleida, Spain
Carles Mateu Piñol
  • Department of Computer Engineering and Digital Design, University of Lleida, Spain

Funding

Josep Maria Salvia Hornos reports funding from Generalitat de Catalunya AGAUR DI-2024-00020. Cèsar Fernández reports funding by the Spanish Ministry of Science and Innovation MCIN/AEI/10.13039/501100011033/ FEDER, UE within the RevTour project (Ref: PID2022-138564OA-I00).

Acknowledgements

We want to thank Alexey Ignatiev and Joao Marques-Silva for participation in tangential MaxSAT research and Elena Barrachina for helping review library documentation.

Supplementary Materials

References

  1. Ignasi Abío, Valentin Mayer-Eichberger, and Peter J Stuckey. Encoding linear constraints with implication chains to cnf. In Proc. of the Int. Conf. on Princ. and Pract. of Constraint Programming (CP), pages 3-11, 2015. URL: https://doi.org/10.1007/978-3-319-23219-5_1.
  2. Tobias Achterberg. Scip: solving constraint integer programs. Mathematical Programming Computation, 1(1):1-41, 2009. URL: https://doi.org/10.1007/S12532-008-0001-1.
  3. Josep Alos, Carlos Ansótegui, Josep M Salvia, and Eduard Torres. Optilog v2: model, solve, tune and run. In 25th Proc. of the Int. Conf. on Theory and Appl. of Satisfiability Testing (SAT), pages 25-1, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.25.
  4. Sahel Alouneh, Sa’ed Abed, Mohammad H Al Shayeji, and Raed Mesleh. A comprehensive study and analysis on sat-solvers: advances, usages and achievements. Artificial Intelligence Review, 52(4):2575-2601, 2019. URL: https://doi.org/10.1007/S10462-018-9628-0.
  5. Benjamin Andres, Benjamin Kaufmann, Oliver Matheis, and Torsten Schaub. Unsatisfiability-based optimization in clasp. In Tech. Commun. of the 28th Int. Conf. on Logic Programming (ICLP), pages 212-221, 2012. URL: https://doi.org/10.4230/LIPIcs.ICLP.2012.211.
  6. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. Sat-based maxsat algorithms. Artificial Intelligence, 196:77-105, 2013. URL: https://doi.org/10.1016/J.ARTINT.2013.01.002.
  7. Carlos Ansótegui and Felip Manya. Mapping problems with finite-domain variables to problems with boolean variables. In Proc. of the Int. Conf. on Theory and Appl. of Satisfiability Testing (SAT), pages 1-15, 2004. URL: https://doi.org/10.1007/11527695_1.
  8. Carlos Ansótegui, Jesus Ojeda, António Pacheco, Josep Pon, Josep M Salvia, and Eduard Torres. Optilog: A framework for sat-based systems. In Proc. of the Int. Conf. on Theory and Appl. of Satisfiability Testing (SAT), pages 1-10, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_1.
  9. Josep Argelich, Chu-Min Li, Felip Manya, and Jordi Planes. The first and second max-sat evaluations. Journal on Satisfiability, 4(2-4):251-278, 2008. URL: https://doi.org/10.3233/SAT190047.
  10. Gilles Audemard and Laurent Simon. On the glucose sat solver. International Journal on Artificial Intelligence Tools, 27(01):1840001, 2018. URL: https://doi.org/10.1142/S0218213018400018.
  11. Florent Avellaneda. Evalmaxsat 2023. MaxSAT Evaluation, 2023:12, 2023. Google Scholar
  12. Tomáš Balyo, Armin Biere, Markus Iser, Carsten Sinz, and Allen Van Gelder. Sat race 2015. Artificial Intelligence, 241:45-65, 2016. URL: https://doi.org/10.1016/J.ARTINT.2016.08.007.
  13. Haniel Barbosa, Clark W. Barrett, et al. cvc5: A versatile and industrial-strength SMT solver. In Proc. of the 28th Int. Conf. on TACAS, volume 13243 of LNS in Computer Science, pages 415-442, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  14. Anton Belov, António Morgado, and Joao Marques-Silva. Sat-based preprocessing for maxsat. In Proc. of the Int. Conf. on Logic for Program., Art. Intell. and Reason. (LPAR), pages 96-111, 2013. URL: https://doi.org/10.1007/978-3-642-45221-5_7.
  15. Jeremias Berg, Emir Demirović, and Peter J Stuckey. Core-boosted linear search for incomplete maxsat. In Proc. of the Int. Conf. on Integr. of Constraint Program., Art. Intell., and Oper. Res. (CPAIOR), pages 39-56, 2019. URL: https://doi.org/10.1007/978-3-030-19212-9_3.
  16. Jeremias Berg, Matti Järvisalo, Ruben Martins, Andreas Niskanen, and Tobias Paxian. Maxsat evaluation 2024: Solver and benchmark descriptions, 2024. Google Scholar
  17. Armin Biere, Tobias Faller, Katalin Fazekas, et al. Cadical 2.0. In International Conference on Computer Aided Verification, pages 133-152, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  18. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. Maxsat, hard and soft constraints. 11.12. 1. Autarkies and qualitative matrix analysis, page 613, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-613.
  19. Miquel Bofill, Jordi Coll, Peter Nightingale, Josep Suy, Felix Ulrich-Oltean, and Mateu Villaret. Sat encodings for pseudo-boolean constraints together with at-most-one constraints. Artificial Intelligence, 302:103604, 2022. URL: https://doi.org/10.1016/J.ARTINT.2021.103604.
  20. 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, page 107195, 2025. URL: https://doi.org/10.1016/J.COR.2025.107195.
  21. Jessica Davies and Fahiem Bacchus. Solving maxsat by solving a sequence of simpler sat instances. In Proc. of the Int. Conf. on Princ. and Pract. of Constraint Programming (CP), pages 225-239, 2011. URL: https://doi.org/10.1007/978-3-642-23786-7_19.
  22. Jessica Davies and Fahiem Bacchus. Exploiting the power of mip solvers in maxsat. In Proc. of the Int. Conf. on Theory and Appl. of Satisfiability Testing (SAT), pages 166-181, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_13.
  23. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In Proc. of the Int. Conf. on Tools and Algorith. for the Constr. and Anal. of Syst. (TACAS), pages 337-340, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  24. Steven Diamond and Stephen Boyd. Cvxpy: A python-embedded modeling language for convex optimization. Journal of Machine Learning Research, 17(83):1-5, 2016. URL: https://jmlr.org/papers/v17/15-408.html.
  25. Niklas Eén and Niklas Sörensson. Translating pseudo-boolean constraints into sat. Journal on Satisfiability, Boolean Modelling and Computation, 2(1-4):1-26, 2006. URL: https://doi.org/10.3233/SAT190014.
  26. Johannes K Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r) evolution of sat. Communications of the ACM, 66(6):64-72, 2023. URL: https://doi.org/10.1145/3560469.
  27. Tias Guns. Increasing modeling language convenience with a universal n-dimensional array, cppy as python-embedded example. In Proc. of the Workshop on Constraint Model. and Reformulation (ModRef), volume 19, 2019. Google Scholar
  28. William E Hart, Carl D Laird, Jean-Paul Watson, David L Woodruff, et al. Pyomo-optimization modeling in python, volume 67. Springer, 2017. Google Scholar
  29. Federico Heras, Javier Larrosa, and Albert Oliveras. Minimaxsat: An efficient weighted max-sat solver. Journal of Artificial Intelligence Research, 31:1-32, 2008. URL: https://doi.org/10.1613/JAIR.2347.
  30. Hao Hu, Mohamed Siala, Emmanuel Hebrard, and Marie-José Huguet. Learning optimal decision trees with maxsat and its integration in adaboost. In Proc. of the 29th Int. Joint Conf. on Artificial Intelligence (IJCAI), pages 1170-1176, 2020. URL: https://doi.org/10.24963/IJCAI.2020/163.
  31. QHJAJ Huangfu and JA Julian Hall. Parallelizing the dual revised simplex method. Mathematical Programming Computation, 10(1):119-142, 2018. URL: https://doi.org/10.1007/S12532-017-0130-5.
  32. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. Pysat: A python toolkit for prototyping with sat oracles. In Proc. of the Int. Conf. on Theory and Appl. of Satisfiability Testing (SAT), pages 428-437, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
  33. Alexey Ignatiev, António Morgado, and João Marques-Silva. Rc2: an efficient maxsat solver. Journal on Satisfiability, Boolean Modelling and Computation, 11(1):53-64, 2019. URL: https://doi.org/10.3233/SAT190116.
  34. Hannes Ihalainen, Jeremias Berg, et al. Refined core relaxation for core-guided maxsat solving. In 27th Proc. of the Int. Conf. on Princ. and Pract. of Constraint Programming (CP), pages 28-1, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.28.
  35. Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Unifying sat-based approaches to maximum satisfiability solving. Journal of Artificial Intelligence Research, 80:931-976, 2024. URL: https://doi.org/10.1613/JAIR.1.15986.
  36. J. S. Roy, Stuart A. Mitchell, and PuLP contributors. PuLP, 2025. Python LP and MILP modeling library. Google Scholar
  37. Christoph Jabs. RustSAT: A library for SAT solving in rust. In 28th Proc. of the Int. Conf. on Theory and Appl. of Satisfiability Testing (SAT), volume 341, pages 15:1-15:13, 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.15.
  38. Christoph Jabs, Jeremias Berg, Andreas Niskanen, and Matti Järvisalo. Maxsat-based bi-objective boolean optimization. In Proc. of the Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), pages 12:1-12:18, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.12.
  39. Mikoláš Janota. Mifumax—a literate maxsat solver: System description. Journal on Satisfiability, Boolean Modelling and Computation, 9(1):83-88, 2014. URL: https://doi.org/10.3233/SAT190103.
  40. Mikoláš Janota, António Morgado, José Fragoso Santos, and Vasco Manquinho. The seesaw algorithm: Function optimization using implicit hitting sets. In Proc. of the Int. Conf. on Princ. and Pract. of Constraint Programming (CP), pages 31:1-31:16, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.31.
  41. Menghua Jiang and Yin Chen. NuWLS-c-IBR: solver description. MaxSAT Evaluation 2024: Solver and Benchmark Descriptions, page 22, 2024. Google Scholar
  42. Saurabh Joshi, Prateek Kumar, Sukrut Rao, and Ruben Martins. Open-wbo-inc: Approximation strategies for incomplete weighted maxsat. Journal on Satisfiability, Boolean Modelling and Computation, 11(1):73-97, 2019. URL: https://doi.org/10.3233/SAT190118.
  43. Dimitri Justeau-Allaire and Charles Prud'Homme. pychoco: all-inclusive python bindings for the choco-solver constraint programming library. Journal of Open Source Software, 10(113):8847, 2025. Google Scholar
  44. Stephen Maher, Matthias Miltenberger, et al. PySCIPOpt: Mathematical programming in python with the SCIP optimization suite. In Mathematical Software, pages 301-307. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-42432-3_37.
  45. Joao Marques-Silva and Jordi Planes. Algorithms for maximum satisfiability using unsatisfiable cores. In Proc. of the Conf. on Design, Autom. and Test in Eur., pages 408-413, 2008. URL: https://doi.org/10.1109/DATE.2008.4484715.
  46. Ruben Martins, Vasco Manquinho, et al. Open-wbo: A modular maxsat solver. In Proc. of the Int. Conf. on Theory and Appl. of Satisfiability Testing (SAT), pages 438-445, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_33.
  47. Clair E Miller, Albert W Tucker, and Richard A Zemlin. Integer programming formulation of traveling salesman problems. Journal of the ACM, 7(4):326-329, 1960. URL: https://doi.org/10.1145/321043.321046.
  48. António Morgado, Carmine Dodaro, and Joao Marques-Silva. Core-guided maxsat with soft cardinality constraints. In Proc. of the Int. Conf. on Princ. and Pract. of Constraint Programming (CP), pages 564-573, 2014. URL: https://doi.org/10.1007/978-3-319-10428-7_41.
  49. Alexander Nadel. Tt-open-wbo-inc: an efficient anytime maxsat solver. Journal on Satisfiability, Boolean Modelling and Computation, 15(1):1-7, 2024. URL: https://doi.org/10.3233/SAT-231504.
  50. Nicholas Nethercote, Peter J Stuckey, Ralph Becket, Sebastian Brand, Gregory J Duck, and Guido Tack. Minizinc: Towards a standard cp modelling language. In Proc. of the Int. Conf. on Princ. and Pract. of Constraint Programming (CP), pages 529-543, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_38.
  51. Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Enabling incrementality in the implicit hitting set approach to maxsat under changing weights. In 27th Proc. of the Int. Conf. on Princ. and Pract. of Constraint Programming (CP), pages 44-1, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.44.
  52. Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Incremental maximum satisfiability. In 25th Proc. of the Int. Conf. on Theory and Appl. of Satisfiability Testing (SAT), pages 14-1, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.14.
  53. Chanseok Oh. COMiniSatPS Pulsar and GHackCOMSPS. In Proceedings of SAT Competition 2017, volume B-2017-1, pages 12-13. University of Helsinki, 2017. Google Scholar
  54. David Orden, José Manuel Giménez, Ivan Marsa-Maestre, and Enrique de la Hoz. Spectrum graph coloring and applications to wi-fi channel assignment. Symmetry, 10(3):65, 2018. URL: https://doi.org/10.3390/SYM10030065.
  55. Shiwei Pan, Yiyuan Wang, et al. An efficient core-guided solver for weighted partial maxsat. In Proc. of the Int. Joint Conf. on Art. Intell. (IJCAI), pages 2647-2656, 2025. URL: https://doi.org/10.24963/IJCAI.2025/295.
  56. Tobias Paxian and Armin Biere. Maxsat fuzzing and delta debugging. Journal of Artificial Intelligence Research, 85, 2026. URL: https://doi.org/10.1613/JAIR.1.19716.
  57. Laurent Perron, Frédéric Didier, and Steven Gay. The cp-sat-lp solver (invited talk). In Proc. of the Int. Conf. on Princ. and Pract. of Constraint Programming (CP), pages 3-1, 2023. URL: https://doi.org/10.4230/LIPIcs.CP.2023.3.
  58. Tobias Philipp and Peter Steinke. Pblib - a library for encoding pseudo-boolean constraints into cnf. In Proc. of the Int. Conf. on Theory and Appl. of Satisfiability Testing (SAT), pages 9-16, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_2.
  59. Marek Piotrów. Uwrmaxsat: Efficient solver for maxsat and pseudo-boolean problems. In Proc. of the 32nd Int. Conf. on Tools with Art. Intell. (ICTAI), pages 132-136. IEEE, 2020. URL: https://doi.org/10.1109/ICTAI50040.2020.00031.
  60. Matthew J Saltzman. Coin-or: an open-source library for optimization. In Programming languages and systems in computational economics and finance, pages 3-32. Springer, 2002. Google Scholar
  61. Josep Maria Salvia Hornos, Cèsar Fernández Camón, and Carles Mateu Piñol. Hermax: MaxSAT Optimization for Python Documentation. Text (visited on 2026-06-29). URL: https://hermax.readthedocs.io/
    full metadata available at: https://doi.org/10.4230/artifacts.26925
  62. Josep Maria Salvia Hornos, Cèsar Fernández Camón, and Carles Mateu Piñol. Hermax: MaxSAT Optimization for Python Pypi Distribution. Software (visited on 2026-06-29). URL: https://pypi.org/project/hermax
    full metadata available at: https://doi.org/10.4230/artifacts.26924
  63. Josep Maria Salvia Hornos, Cèsar Fernández Camón, and Carles Mateu Piñol. josalhor/hermax. Software (visited on 2026-05-26). URL: https://github.com/josalhor/hermax
    full metadata available at: https://doi.org/10.4230/artifacts.25966
  64. Josep Maria Salvia Hornos, Cèsar Fernández Camón, Carles Mateu Piñol, Joao Marques-Silva, Ivet Rafegas Fonoll, and Josep Cirera Balcells. Modelling and optimising switching on a physical binary sorter. Annals of Operations Research, pages 1-22, 2026. URL: https://doi.org/10.1007/S10479-025-06903-2.
  65. Tobias Seufert, Felix Winterer, et al. Everything you always wanted to know about generalization of proof obligations in bit-level pdr. In MBMV. Workshop, pages 144-147, 2024. URL: https://doi.org/10.1109/TCAD.2022.3198260.
  66. Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, and Mutsunori Banbara. Compiling finite linear csp into sat. Constraints, 14(2):254-272, 2009. URL: https://doi.org/10.1007/S10601-008-9061-0.
  67. Johannes P Wallner, Andreas Niskanen, and Matti Järvisalo. Complexity results and algorithms for extension enforcement in abstract argumentation. Journal of Artificial Intelligence Research, 60:1-40, 2017. URL: https://doi.org/10.1613/JAIR.5415.
  68. Jiongzhi Zheng, Zhuo Chen, Chu-Min Li, and Kun He. Rethinking the soft conflict pseudo boolean constraint on maxsat local search solvers. In Proc. of the Int. Joint Conf. on Art. Intell. (IJCAI), 2024. URL: https://www.ijcai.org/proceedings/2024/220.
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