Vectors, Matrices and Dicts#

The modelling layer provides structured containers for typed variables:

  • vectors

  • matrices

  • keyed dictionaries

These containers keep models readable and easy to decode.

Vectors#

Constructors:

  • model.bool_vector(name, length)

  • model.int_vector(name, length, lb, ub)

  • model.enum_vector(name, length, choices, nullable=False)

Vectors support indexing, iteration, and typed helpers.

BoolVector helpers#

BoolVector provides cardinality helpers:

  • at_most_one()

  • exactly_one()

  • at_least_one()

Example:

row = model.bool_vector("row", 4)
model &= row.exactly_one()

IntVector helpers#

IntVector provides higher-level finite-domain constraints:

  • all_different(backend=\"auto\")

  • increasing() (nondecreasing)

  • lexicographic_less_than(other)

  • max(name=None)

  • min(name=None)

  • upper_bound(name=None)

  • lower_bound(name=None)

  • running_max(name=None)

  • running_min(name=None)

Variable index: vec[idx]#

IntVector supports element constraints with a variable index:

vals = model.int_vector("vals", length=3, lb=0, ub=10)
idx = model.int("idx", 0, 3)
a = model.int("a", 0, 10)

model &= (vals[idx] == a)

This compiles as conditional branch constraints:

\[(idx = i) \Rightarrow (vals_i \; OP \; rhs)\]

for each index value i and comparator OP.

Supported comparators on vals[idx]:

  • ==, !=

  • <=, <, >=, >

RHS currently supports:

  • integer constants

  • IntVar

Index coverage rules:

  • idx.lb must be non-negative

  • vector length must cover the index domain span [idx.lb, idx.ub]

Constraint helpers (all_different, increasing, lexicographic_less_than) return ClauseGroup.

The aggregate helpers:

  • max(name=None)

  • min(name=None)

  • upper_bound(name=None)

  • lower_bound(name=None)

  • running_max(name=None)

  • running_min(name=None)

return lazy derived integer expressions. They do not change the model.

Use Model methods for explicit eager materialization:

  • model.max(vec_or_items, name=None)

  • model.min(vec_or_items, name=None)

  • model.upper_bound(vec_or_items, name=None)

  • model.lower_bound(vec_or_items, name=None)

These methods also accept plain list/tuple of IntVar.

Running Prefix#

IntVector.running_max() and IntVector.running_min() return materialized prefix aggregates:

\[\begin{split}\begin{aligned} r_i^{\max} &= \max(x_0, \dots, x_i) \\ r_i^{\min} &= \min(x_0, \dots, x_i) \end{aligned}\end{split}\]

These helpers avoid rebuilding max(self[:i+1]) / min(self[:i+1]) at each prefix (O(N^2) clauses). They use a cumulative fold:

\[r_i^{\max} = \max(r_{i-1}^{\max}, x_i), \qquad r_i^{\min} = \min(r_{i-1}^{\min}, x_i)\]

Each step uses model.max(...) / model.min(...).

Example:

timeline = model.int_vector("level", 5, lb=0, ub=100)
watermark = timeline.running_max("watermark")
valley = timeline.running_min("valley")

model &= (watermark[3] <= 50)
model &= (valley[4] >= 10)

IntVector.all_different() backends#

IntVector.all_different() accepts a backend selector:

  • backend=\"auto\" (default): currently aliases to \"pairwise\"

  • backend=\"pairwise\": pairwise x_i != x_j constraints

  • backend=\"bipartite\": exact-value channeling + column at-most-one constraints

The bipartite backend currently requires:

  • a common domain across the vector

  • domain size at least the vector length

Min/Max Aggregates#

IntVector.max() / IntVector.min() are lazy wrappers. The actual ladder encoding is built by model.max(...) / model.min(...) when the aggregate is materialized (for example in model &= ... or in a PB constraint during Stage 2 compilation).

If t_k denotes the threshold predicate (x >= k), then:

\[\begin{split}\begin{aligned} z = \max(x_1,\dots,x_n) &\iff z_{\ge k} \leftrightarrow \bigvee_{i=1}^n x_{i,\ge k} \\ z = \min(x_1,\dots,x_n) &\iff z_{\ge k} \leftrightarrow \bigwedge_{i=1}^n x_{i,\ge k} \end{aligned}\end{split}\]

Example:

xs = model.int_vector("x", 4, lb=0, ub=10)
xmax = xs.max("xmax")        # lazy derived int expression
xmin = xs.min("xmin")        # lazy derived int expression
model &= (xmin >= 2)
model &= (xmax <= 7)

xmax2 = model.max(xs, name="xmax2")
xmin2 = model.min(xs, name="xmin2")

The output domain is inferred from the operands:

  • max uses [max(lb_i), max(ub_i))

  • min uses [min(lb_i), min(ub_i))

One-Sided Bounds#

IntVector.upper_bound() / IntVector.lower_bound() are lazy wrappers. The eager implementations are model.upper_bound(...) and model.lower_bound(...), which build a fresh integer variable with only one direction of the aggregate relation:

\[\begin{split}\begin{aligned} u = \mathrm{upper\_bound}(x_1,\dots,x_n) &\Rightarrow u \ge x_i \quad \forall i \\ \ell = \mathrm{lower\_bound}(x_1,\dots,x_n) &\Rightarrow \ell \le x_i \quad \forall i \end{aligned}\end{split}\]

These are weaker than exact max/min but cheaper: one direction only.

Example:

xs = model.int_vector("x", 4, lb=0, ub=10)
ubv = model.upper_bound(xs, name="ubv")
model.obj[1] += ubv

EnumVector helpers#

EnumVector.all_different(backend=\"auto\") is supported and returns a ClauseGroup.

Backends:

  • backend=\"auto\" (default): aliases to \"bipartite\"

  • backend=\"bipartite\": column-wise at-most-one over enum choice literals

  • backend=\"pairwise\": pairwise enum inequality constraints

For nullable enums, the current bipartite implementation falls back to the pairwise backend so that the None case is handled correctly without adding a dedicated is_none indicator literal.

Allowed combinations: Vector.is_in(rows)#

Typed vector views support allowed-combinations constraints:

  • BoolVector.is_in(rows)

  • EnumVector.is_in(rows)

  • IntVector.is_in(rows)

This is the model-layer table constraint:

cpu = model.int("cpu", 0, 6)
ram = model.int("ram", 0, 6)
mobo = model.int("mobo", 0, 6)

spec = model.vector([cpu, ram, mobo])
model &= spec.is_in([
    (1, 2, 1),
    (2, 4, 2),
    (3, 4, 3),
])

Arbitrary typed vector views#

Use model.vector(items) to build a typed vector view from an arbitrary subset of variables:

region = model.vector([grid[r, c] for r in rows for c in cols])
model &= region.all_different()

This is useful for irregular subsets such as Sudoku subgrids, selected resources, or custom neighborhoods, and for combining subset views with .is_in(rows).

Matrices#

Constructors:

  • model.bool_matrix(name, rows, cols)

  • model.int_matrix(name, rows, cols, lb, ub)

  • model.enum_matrix(name, rows, cols, choices, nullable=False)

Matrix helpers#

All matrix types support:

  • row(i)

  • col(j)

  • flatten()

and also NumPy indexing:

  • m[r, c] -> cell

  • m[r, :] -> typed row vector

  • m[:, c] -> typed column vector

  • m[r0:r1, c0:c1] -> typed submatrix view

  • m[r0:r1, c0:c1].flatten() -> typed vector

Example (Sudoku subgrid):

grid = model.int_matrix("cell", 9, 9, lb=1, ub=10)
model &= grid[0:3, 0:3].flatten().all_different()

This is the intended NumPy syntax for rectangular subsets.

Keyed Dictionaries#

Constructors:

  • model.bool_dict(name, keys)

  • model.int_dict(name, keys, lb, ub)

  • model.enum_dict(name, keys, choices, nullable=False)

These are useful when natural indexing is not numeric.

Example:

routers = [10, 20, 30]
state = model.enum_dict("router_state", routers, choices=["1", "2", "3"], nullable=True)
model &= ~(state[10] == "1") | ~(state[20] == "1")

This pattern is used in examples/wifi_model.py. Combined with EnumVar.is_in(...) it gives a compact API for category subsets.

Decode Support#

Model solution auto-decodes containers:

  • vector -> Python list

  • matrix / matrix view -> nested list

  • dict -> Python dict keyed by original keys

Example:

examples/model/21_decode_collections.py#
from hermax.model import Model

m = Model()

vec = m.int_vector("vec", length=3, lb=0, ub=5)
mat = m.int_matrix("mat", rows=2, cols=2, lb=0, ub=5)
flags = m.bool_dict("flag", keys=["r1", "r2"])
mode = m.enum_dict("mode", keys=["r1", "r2"], choices=["eco", "boost"], nullable=True)

m &= (vec[0] == 1)
m &= (vec[1] == 3)
m &= (vec[2] == 2)

m &= (mat[0, 0] == 2)
m &= (mat[0, 1] == 4)
m &= (mat[1, 0] == 1)
m &= (mat[1, 1] == 0)

m &= flags["r1"]
m &= ~flags["r2"]

m &= (mode["r1"] == "eco")
m &= (mode["r2"] == "boost")

r = m.solve()
assert r.ok

print("vec        =", r[vec])
print("mat        =", r[mat])
print("mat col 1  =", r[mat[:, 1]])
print("flags      =", r[flags])
print("mode       =", r[mode])

Example output#

$ python examples/model/21_decode_collections.py
vec        = [1, 3, 2]
mat        = [[2, 4], [1, 0]]
mat col 1  = [4, 0]
flags      = {'r1': True, 'r2': False}
mode       = {'r1': 'eco', 'r2': 'boost'}