Hermax: MaxSAT Optimization for Python#

Hermax is a pormanteau of Hermes and MaxSAT.

In Greek mythology, Hermes is the messenger between the worlds of gods and mortals. Similarly, Hermax is conceived as the bridge between Python, the divine world where messages are sent down the stack, and C/C++, the mortal world with it’s struggles and hardships, where performance is critical.

Who Is This For?#

Hermax is for combinatorially hard problems where:

finding even a good base solution is already difficult
the search state is mostly boolean

This is usually a better fit than MILP tooling when your problem is not mainly about floating-point structure, large integer arithmetic, or strong LP relaxations. In those cases, a MILP such as PuLP, SCIP, or Gurobi is often the more natural first choice.

If your problem is highly combinatorial but can benefit from a broader black-box CP approach, CP-SAT or MiniZinc may also be a good alternative.

Hermax is especially relevant for:

engineers building reliable (mostly boolean) optimization problems
users who already work with clauses, WCNF, or incremental solver APIs
researchers comparing MaxSAT backends behind a common Python interface

Start Here#

Quick Start if you want the fastest path to a working Hermax model and a direct solver example.
Examples if you want solver examples such as UWrMaxSAT, RC2, graph colouring, scheduling, and CVRP.
Modelling if you want the modelling compiler, runnable examples, and advanced modelling tricks.

Useful Next Steps#

Portfolio Solver for multi-solver execution and preset portfolios.
Incremental Solvers for incremental MaxSAT workflows and assumptions.
Bindings Reference for backend-specific notes and solver availability.
API Reference if you want the full API reference.
Changelog for versioned user-facing changes.

Citation#

If you use Hermax in research, please cite:

@InProceedings{salviahornos_et_al:LIPIcs.SAT.2026.41,
  author = {Salvia Hornos, Josep Maria and Fern\'{a}ndez Cam\'{o}n, C\`{e}sar and Mateu Pi\~{n}ol, Carles},
  title = {{Hermax: A Unified MaxSAT Library}},
  booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages = {41:1--41:13},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN = {978-3-95977-431-4},
  ISSN = {1868-8969},
  year = {2026},
  volume = {377},
  editor = {Ignatiev, Alexey and Szeider, Stefan},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f\"{u}r Informatik},
  address = {Dagstuhl, Germany},
  URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.41},
  URN = {urn:nbn:de:0030-drops-263478},
  doi = {10.4230/LIPIcs.SAT.2026.41},
  annote = {Keywords: MaxSAT, Incremental Solving, IPAMIR, Python, Constraint modelling}
}

See Acknowledgments for backend solver citations and other project references.