Metadata-Version: 2.4
Name: hermax
Version: 1.2.4
Summary: A Python library of incremental MaxSAT solvers
Home-page: https://github.com/josalhor/hermax
Author: Josep Maria Salvia Hornos
Author-email: josh.salvia@gmail.com
License: Apache-2.0
Project-URL: Documentation, https://hermax.readthedocs.io
Project-URL: Repository, https://github.com/josalhor/hermax
Project-URL: Issues, https://github.com/josalhor/hermax/issues
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Topic :: Scientific/Engineering
Description-Content-Type: text/markdown
License-File: LICENSE
License-File: NOTICE
Requires-Dist: python-sat
Provides-Extra: optilog
Requires-Dist: optilog==0.6.1; extra == "optilog"
Dynamic: author
Dynamic: author-email
Dynamic: classifier
Dynamic: description
Dynamic: description-content-type
Dynamic: home-page
Dynamic: license
Dynamic: license-file
Dynamic: project-url
Dynamic: provides-extra
Dynamic: requires-dist
Dynamic: summary

# Hermax: MaxSAT Optimization for Python

<p align="center">
  <a href="https://pypi.org/project/hermax/"><img alt="PyPI version" src="https://img.shields.io/pypi/v/hermax.svg"></a>
  <a href="https://pypi.org/project/hermax/"><img alt="PyPI wheel" src="https://img.shields.io/pypi/wheel/hermax.svg"></a>
  <a href="https://pypi.org/project/hermax/"><img alt="Python versions" src="https://img.shields.io/pypi/pyversions/hermax.svg"></a>
  <a href="LICENSE"><img alt="License: Apache-2.0" src="https://img.shields.io/badge/License-Apache%202.0-blue.svg"></a>
  <a href="https://hermax.readthedocs.io/en/latest/?badge=latest"><img alt="Documentation Status" src="https://readthedocs.org/projects/hermax/badge/?version=latest"></a>
  <br>
  <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.41"><img alt="Paper: SAT 2026" src="https://img.shields.io/badge/Paper-SAT%202026-007C7A"></a>
  <img alt="Windows supported" src="https://img.shields.io/badge/Windows-supported-0078D6?logo=windows">
  <img alt="Linux supported" src="https://img.shields.io/badge/Linux-supported-FCC624?logo=linux&amp;logoColor=black">
  <img alt="macOS supported" src="https://img.shields.io/badge/macOS-supported-000000?logo=apple">
</p>

![Hermax Banner](https://raw.githubusercontent.com/josalhor/hermax/main/images/banner.png)

Hermax is a Python bridge to high-performance MaxSAT backends, with a unified
IPAMIR-inspired interface for hard clauses, soft literals, assumptions, and
iterative optimization workflows.

## Why Hermax

- High-level modeling API (`hermax.model`) with typed variables, vectors, matrices, intervals, and lazy arithmetic.
- Unified API across heterogeneous MaxSAT engines.
- Incremental and non-incremental solver families
- Scientific and reproducible workflow
- Native compatibility with [PySAT](https://pysathq.github.io/)

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](https://pypi.org/project/PuLP/),
[SCIP](https://www.scipopt.org/), or [Gurobi](https://www.gurobi.com/) 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](https://developers.google.com/optimization/cp/cp_solver)
may also be a good alternative.

Hermax is especially relevant for:

* engineers building repeated optimization workflows around hard clauses, soft
  literals, assumptions, and iterative solve loops,
* users who already work with clauses, WCNF, or incremental solver-style APIs,
  and
* researchers comparing MaxSAT backends behind a common Python interface.

## Installation

Core install:

```bash
pip install hermax
```
- User and API docs: https://hermax.readthedocs.io


## Modeling Example

```python
from hermax.model import Model

m = Model()

# Decision variables
x = m.int_vector("x", length=4, lb=0, ub=6)       # integer domain [0, 6]
use_bonus = m.bool("use_bonus")

# Hard constraints
m &= x.all_different()
m &= (x[0] + x[1] <= x[2] + 2)
m &= (x[3] >= 2).only_if(use_bonus)

# Soft objective terms
m.obj[5] += (x[0] == 1)
m.obj[3] += ~use_bonus

r = m.solve()  # auto-routes SAT/MaxSAT based on model content
print(r.status, r.cost)
```

## Incremental MaxSAT Example

```python
from hermax.incremental import UWrMaxSAT

solver = UWrMaxSAT()
solver.add_clause([1, 2])   # hard
solver.set_soft(-1, 10)     # soft weight
solver.set_soft(-1, 6)      # update weight (last-wins)

ok = solver.solve(assumptions=[-2])
print("status:", solver.get_status().name)
if ok:
    print("cost:", solver.get_cost())
    print("model:", solver.get_model())
```

## Citation

If you use Hermax in research, please cite:

```bibtex
@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}
}
```

Please also cite the backend solver papers relevant to your experiments; see
the [documentation acknowledgments](https://hermax.readthedocs.io/en/latest/acknowledgments.html),
`CITATION.cff`, and `NOTICE` for the relevant references.

## License

This repository is licensed under Apache License 2.0. See `LICENSE`.
Third-party integrated solvers may have additional license terms.
