Quick Start#

Installation#

From PyPI:

pip install hermax

Basic Usage#

Start with the modelling path. This is the entry point if your problem is already expressed in terms of decisions, constraints, and an objective.

Model Example#

This CVRP example shows the usual Hermax workflow with MTZ load constraints [1]:

  1. declare variables,

  2. add hard constraints,

  3. add soft costs,

  4. solve and inspect the selected decisions.

Problem#

_images/cvrp_flat_problem.svg
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#

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

Solution#

_images/cvrp_flat_solution.svg

Incremental MaxSAT Example#

If you already work with literals and clauses, use the solver API without going through the modelling layer. This version uses pysat.formula.IDPool from PySAT [2] to manage variable identifiers and hermax.incremental.UWrMaxSAT [3] as the backend.

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#

Direct solver example 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]

References#

Next#

If you want to continue with runnable material, the next pages to look at are: