Examples

All examples below are executable Python files in examples/.

Modelling Gallery

For an introduction of the modelling examples (problem, new primitives, model, code, and output), see:

• Modelling Examples

For a gallery focused on optimization modelling tricks (piecewise costs, binning, ladder constraints, fast paths, interval makespan, and all_different backends), see:

• Advanced Modelling Examples

For a small gallery of classic NP-hard problems, see:

• NP-Hard Problems

Soft-cost polarity note

Hermax examples use two closely related, but easy-to-confuse, APIs for soft constraints:

• IPAMIR soft literals (set_soft(lit, w) / add_soft_unit(lit, w)): the cost is paid when the literal is false. For example, set_soft(-x, 5) means paying 5 when x=True.

• WCNF soft clauses (WCNF.append(clause, weight=...)): the cost is paid when the clause is violated. For a unit clause [x], that means paying when x=False.

CVRP

This is a capacitated vehicle routing (CVRP) example with depot-to-customer routes, capacity tracking, and MTZ load constraints [5].

Related API: hermax.model.Model.

Problem

examples/cvrp_flat.py

import math

from hermax.model import Model


coords = [(0, 0), (2, 4), (5, 2), (7, 6), (1, 5)]
demands = [0, 4, 5, 3, 5]
capacity = 10
vehicles = 2
n = len(demands)

dist = [
    [int(math.hypot(ax - bx, ay - by) * 10) for bx, by in coords]
    for ax, ay in coords
]

m = Model()
edge = m.bool_matrix("edge", n, n)
load = m.int_vector("load", n, lb=0, ub=capacity)

m &= sum(edge.row(0)) == vehicles
m &= sum(edge.col(0)) == vehicles
m &= load[0] == 0

for i in range(n):
    m &= ~edge[i][i]
    if i > 0:
        m &= edge.row(i).exactly_one()
        m &= edge.col(i).exactly_one()
        m &= load[i] >= demands[i]

for i in range(n):
    for j in range(1, n):
        if i != j:
            m &= (load[i] + demands[j] <= load[j]).only_if(edge[i][j])

for i in range(n):
    for j in range(n):
        if i != j:
            m.obj += dist[i][j] * edge[i][j]

res = m.solve()

print("status:", res.status)
print("cost:", res.cost)
for i in range(n):
    for j in range(n):
        if res[edge[i][j]]:
            print(f"{i} -> {j}")

Output

$ python examples/cvrp_flat.py
status: optimum
cost: 297
0 -> 1
0 -> 3
1 -> 4
2 -> 0
3 -> 2
4 -> 0

Solution

Incremental MaxSAT

Below is the smallest Hermax workflow with Incremental MaxSAT: add hard constraints, assign soft penalties, update a soft weight (last write wins), and solve under assumptions. This is the mental model for the IPAMIR API used across the library, using UWrMaxSAT [1].

Related API: hermax.incremental.UWrMaxSAT.

examples/quickstart_uwrmaxsat.py

from pysat.formula import IDPool

from hermax.incremental import UWrMaxSAT

solver = UWrMaxSAT()
vpool = IDPool(start_from=1)

x1 = vpool.id("x1")
x2 = vpool.id("x2")
x3 = vpool.id("x3")

# Hard clauses
solver.add_clause([x1, x2])   # x1 OR x2: at least one of x1, x2 must be true
solver.add_clause([-x1, x3])  # (NOT x1) OR x3: if x1 is true, x3 must also be true

# Soft literals
solver.set_soft(-x1, 1)       # pay 1 if x1=True
solver.set_soft(-x2, 4)       # pay 4 if x2=True
solver.set_soft(x3, 2)        # pay 2 if x3=False
solver.set_soft(-x3, 1)       # pay 1 if x3=True

print("Solve with no assumptions:")
ok = solver.solve()
print("  feasible:", ok)
if ok:
    print("  status:", solver.get_status().name)
    print("  cost:", solver.get_cost())
    print("  model:", solver.get_model())

print("Solve with assumption [-x1] (force x1=False):")
ok = solver.solve(assumptions=[-x1])
print("  feasible:", ok)
if ok:
    print("  status:", solver.get_status().name)
    print("  cost:", solver.get_cost())
    print("  model:", solver.get_model())

solver.set_soft(-x3, 7)       # update the previous penalty on x3=True (last write wins)

print("Solve after updating weight on -x3 from 1 to 7:")
ok = solver.solve()
print("  feasible:", ok)
if ok:
    print("  status:", solver.get_status().name)
    print("  cost:", solver.get_cost())
    print("  model:", solver.get_model())

Output

$ python examples/quickstart_uwrmaxsat.py
Solve with no assumptions:
  feasible: True
  status: OPTIMUM
  cost: 2
  model: [1, -2, 3]
Solve with assumption [-x1] (force x1=False):
  feasible: True
  status: OPTIMUM
  cost: 5
  model: [-1, 2, 3]
Solve after updating weight on -x3 from 1 to 7:
  feasible: True
  status: OPTIMUM
  cost: 6
  model: [-1, 2, -3]

RC2

Use this if you already have formulas in PySAT’s WCNF format and want to run them through Hermax without rewriting your formula-building code. It also shows the non-incremental/rebuild wrapper style, which keeps the same API but is a better fit for one-time solves than repeated incremental queries. This example uses PySAT’s WCNF representation [3] together with RC2 [2].

Related API: hermax.non_incremental.RC2, RC2 Family.

examples/non_incremental_rc2_reentrant.py

from pysat.formula import IDPool, WCNF

from hermax.non_incremental import RC2

wcnf = WCNF()
vpool = IDPool(start_from=1)
a = vpool.id("A")
b = vpool.id("B")
c = vpool.id("C")

# Hard clauses
wcnf.append([-a, -b])  # (NOT A) OR (NOT B): A and B cannot both be true
wcnf.append([b, c])    # B OR C: at least one of them must be true

# Soft clauses
wcnf.append([a], weight=4)  # soft clause [A]: pay 4 if A=False
wcnf.append([b], weight=2)  # soft clause [B]: pay 2 if B=False
wcnf.append([c], weight=1)  # soft clause [C]: pay 1 if C=False

solver = RC2(formula=wcnf)
ok = solver.solve()
print("feasible:", ok)
if ok:
    print("status:", solver.get_status().name)
    print("cost:", solver.get_cost())
    print("model:", solver.get_model())

Output

$ python examples/non_incremental_rc2_reentrant.py
feasible: True
status: OPTIMUM
cost: 2
model: [1, -2, 3]

Load from WCNF Formula

Use this constructor path when your formula is already built elsewhere and you want to hand the whole WCNF to a solver instead of replaying clause additions manually. This is useful when the formula already comes from a PySAT-based workflow [3].

Related API: hermax.incremental.EvalMaxSAT.

examples/load_wcnf_formula.py

from pysat.formula import IDPool, WCNF

from hermax.incremental import EvalMaxSAT


wcnf = WCNF()
vpool = IDPool(start_from=1)
a = vpool.id("A")
b = vpool.id("B")
c = vpool.id("C")

wcnf.append([a, b])          # A OR B: at least one must be true
wcnf.append([-a, c])         # (NOT A) OR C: if A then C
wcnf.append([-b], weight=2)  # soft literal -B: pay 2 if B=True
wcnf.append([-c], weight=1)  # soft literal -C: pay 1 if C=True

solver = EvalMaxSAT(formula=wcnf)
ok = solver.solve()
print("feasible:", ok)
if ok:
    print("status:", solver.get_status().name)
    print("cost:", solver.get_cost())
    print("model:", solver.get_model())

Output

$ python examples/load_wcnf_formula.py
feasible: True
status: OPTIMUM
cost: 1
model: [1, -2, 3]

OptiLog Compatibility

Use this when pipelines produce OptiLog formulas and need to solve them in Hermax without rewriting them into PySAT. This example is specifically about OptiLog interoperability [4].

Related API: hermax.incremental.UWrMaxSAT. External docs: OptiLog documentation.

OptiLog has its own licensing model and is an optional dependency of Hermax.

examples/optilog_formula_compat.py

import importlib.util

from hermax.incremental import UWrMaxSAT

if importlib.util.find_spec("optilog") is None:
    raise RuntimeError(
        """OptiLog is not installed.
Install: pip install "hermax[optilog]"."""
    )

from optilog.formulas import WCNF as OptiWCNF

formula = OptiWCNF()
formula.extend_vars(2)
a = 1
b = 2
formula.add_clause([a, b])  # A OR B: at least one variable must be true
formula.add_clauses([[-a], [-b]], 1)  # soft literals: pay 1 if A=True or B=True

solver = UWrMaxSAT(formula=formula)
ok = solver.solve()
print("status:", solver.get_status().name)
if ok:
    print("cost:", solver.get_cost())
    print("model:", solver.get_model())

Output

$ python examples/optilog_formula_compat.py
status: OPTIMUM
cost: 1
model: [-1, 2]

Custom Portfolio

Use this when a portfolio is needed: combine a complete solver with a fast incomplete solver, run both in isolated processes, and let the portfolio return the first optimal result, or the best valid result before timeout otherwhise.

Related API: hermax.portfolio.PortfolioSolver, Portfolio Solver.

examples/portfolio_mixed.py

from pysat.formula import IDPool, WCNF

from hermax.non_incremental import CGSSSolver
from hermax.non_incremental.incomplete import Loandra
from hermax.portfolio import PortfolioSolver


wcnf = WCNF()
vpool = IDPool(start_from=1)
a = vpool.id("A")
b = vpool.id("B")
wcnf.append([a, b])          # A OR B: at least one variable must be true
wcnf.append([-a, -b])        # (NOT A) OR (NOT B): A and B cannot both be true
wcnf.append([-a], weight=5)  # soft literal -A: pay 5 if A=True
wcnf.append([-b], weight=2)  # soft literal -B: pay 2 if B=True

portfolio = PortfolioSolver(
    [CGSSSolver, Loandra],
    formula=wcnf,
    per_solver_timeout_s=3.0,
    overall_timeout_s=5.0,
    max_workers=2,
    selection_policy="first_optimal_or_best_until_timeout",
)

ok = portfolio.solve()
print("feasible:", ok)
print("status:", portfolio.get_status().name)
if ok:
    print("cost:", portfolio.get_cost())
    print("model:", portfolio.get_model())

Output

$ python examples/portfolio_mixed.py
feasible: True
status: OPTIMUM
cost: 2
model: [-1, 2]

Default Portfolios

Use this when solver lists are not curated by hand. The preset constructors auto-discover backends from Hermax namespaces and build:

• A complete-only portfolio, or

• A mixed performance portfolio

This is the fastest way to get a performance boost.

Related API: hermax.portfolio.CompletePortfolioSolver, hermax.portfolio.PerformancePortfolioSolver, Portfolio Solver.

examples/portfolio_presets.py

from pysat.formula import IDPool

from hermax.portfolio import PortfolioSolver

vpool = IDPool(start_from=1)
x1 = vpool.id("x1")
x2 = vpool.id("x2")

complete_portfolio = PortfolioSolver.complete(
    per_solver_timeout_s=2.0,
    overall_timeout_s=4.0,
    max_workers=2,
)

complete_portfolio.add_clause([x1, x2])     # x1 OR x2: at least one must be true
complete_portfolio.add_clause([-x1, -x2])   # (NOT x1) OR (NOT x2): at most one is true
complete_portfolio.add_soft_unit(-x1, 4)    # pay 4 if x1=True
complete_portfolio.add_soft_unit(-x2, 1)    # pay 1 if x2=True

ok = complete_portfolio.solve()
print("complete preset feasible:", ok)
print("complete preset status:", complete_portfolio.get_status().name)
if ok:
    print("complete preset cost:", complete_portfolio.get_cost())



performance_portfolio = PortfolioSolver.performance(
    per_solver_timeout_s=2.0,
    overall_timeout_s=4.0,
    max_workers=2,
    selection_policy="first_valid",
)

performance_portfolio.add_clause([x1])      # x1: force x1=True
performance_portfolio.add_soft_unit(-x1, 3) # pay 3 because x1 is forced true

ok2 = performance_portfolio.solve()
print("performance preset feasible:", ok2)
print("performance preset status:", performance_portfolio.get_status().name)
if ok2:
    print("performance preset cost:", performance_portfolio.get_cost())

Output

$ python examples/portfolio_presets.py
complete preset feasible: True
complete preset status: OPTIMUM
complete preset cost: 1
performance preset feasible: True
performance preset status: OPTIMUM
performance preset cost: 3

References

[1]

Marek Piotrów. UWrMaxSat: Efficient Solver for MaxSAT and Pseudo-Boolean Problems. ICTAI 2020.

[2]

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva. RC2: An Efficient MaxSAT Solver. JSAT 11(1), 2019.

[3] (1,2)

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva. PySAT: A Python Toolkit for Prototyping with SAT Oracles. SAT 2018.

[4]

Carlos Ansótegui, Jesus Ojeda, António Pacheco, Josep Pon, Josep M. Salvia, Eduard Torres. Optilog: A framework for SAT-based systems. SAT 2021.

[5]

Josep Alos, Carlos Ansótegui, Josep M. Salvia, Eduard Torres. Optilog V2: model, solve, tune and run. SAT 2022.