Modelling API Reference#

Documents the public API surface of hermax.model.

Module#

Core Objects#

class hermax.model.Model#

Pure-Python SAT/MaxSAT modeling container.

Model is the mutable sink for hard constraints and weighted soft constraints. All other modeling objects are immutable-by-operator.

ALLOW_NEGATIVE_OBJECTIVE_OFFSETS = True#

SOFT_DEDUP_ENABLED = True#

SOFT_GCD_OPTIMIZATION_ENABLED = True#

MERGE_PB_OPTIMIZATION_ENABLED = False#

DEBUG_NONE = 0#

DEBUG_DELTA = 1#

DEBUG_COMPILE = 2#

DEBUG_VERBOSE = 3#

__init__()#

set_debug(level=1, stream=None)#

Configure model debug tracing.

Levels:

0: disabled
1: delta-level logs (hard/soft additions, weight updates)
2: compiler summaries (normalized PB/Card form, cache hit/miss)
3: verbose clause dumps

Parameters:: level (int)
Return type:: None

set_merge_pb_optimization(enabled=True)#

Enable or disable deferred PB batch merge optimization.

Parameters:: enabled (bool)
Return type:: None

set_rebuild_on_interrupt(enabled=True)#

Allow a live incremental backend to rebuild after interruption.

The setting is forwarded when a MaxSAT backend is bound. It is only meaningful for native incremental solvers that explicitly support it.

Parameters:: enabled (bool)
Return type:: None

set_kmerge_config(config=None, **kwargs)#

Replace or update the K-MERGE heuristic configuration.

Parameters:: config (KMergeConfig | None)
Return type:: None

enable_profiling(enabled=True)#

Enable or disable structured encoding profiling.

Parameters:: enabled (bool)
Return type:: None

get_encoding_profile()#

Return the current encoding profile object, if enabled.

Return type:: EncodingProfile | None

profile_scope(kind, *, label=None, metadata=None)#

Profile a block of encoding work as a nested event.

Parameters:

kind (str)
label (str | None)
metadata (Mapping[str, object] | None)

set_objective_offset_policy(*, allow_negative)#

Set objective constant-offset policy for this model instance.

Parameters:: allow_negative (bool) – If False, objective operations that require a negative internal constant offset raise ValueError.
Return type:: None

Notes

This policy is used by both flat objectives (model.obj) and tiered objectives (model.tier_obj).

set_soft_dedup(enabled)#

Enable or disable duplicate soft-clause accumulation on add_soft.

Parameters:: enabled (bool)
Return type:: None

set_soft_gcd_optimization(enabled)#

Enable or disable one-shot MaxSAT soft-weight GCD scaling.

Parameters:: enabled (bool)
Return type:: None

set_auto_pb_commit(enabled)#

Enable or disable immediate materialization of deferred PB/Card clauses.

By default, pure Boolean PB/Card fallback encodings are deferred until _commit_pb(), export, or solve. Enabling this toggle restores eager commit behavior for those deferred constraints while leaving the defer-capable architecture in place.

Parameters:: enabled (bool)
Return type:: None

set_objective_precision(*, decimals)#

Enable/adjust decimal precision for objective-side soft weights.

Notes

Precision applies to objective entry points (model.obj, model.tier_obj, and add_soft weight parsing). PB/Card arithmetic constraints still require integer coefficients and constants.

Parameters:: decimals (int)
Return type:: None

property obj: _ObjectiveProxy#

Objective proxy for additive and replacement objective operations.

Notes

model.obj and model.tier_obj are mutually exclusive. Clear one objective mode before activating the other.

property tier_obj: _TierObjectiveProxy#

Lexicographic objective proxy (tiered optimization).

Notes

model.tier_obj cannot be used together with flat objective operations (model.obj/add_soft).

fresh_internal_bool(debug_name=None)#

Return a fresh internal helper literal.

Internal helpers are intentionally not added to the public model registry. debug_name is advisory only and does not affect identity.

Parameters:: debug_name (str | None)
Return type:: Literal

canonical_internal_bool(key, debug_name=None)#

Return a canonical reusable internal helper literal for key.

Repeated requests with the same semantic key return the same internal literal. The helper remains hidden from the public registry.

Parameters:

key (object)
debug_name (str | None)

Return type:

Literal

bool(name=None)#

Create a Boolean variable and return its positive literal.

Parameters:: name (str | None) – Optional user-facing identifier. If omitted, an anonymous variable name is generated.
Return type:: Literal

enum(name, choices, nullable=False)#

Create an enum variable with the given choices.

Non-nullable enums are exactly-one; nullable enums are at-most-one and decode to None when no choice is selected.

Parameters:

name (str)
choices (Sequence[str])
nullable (bool)

Return type:

EnumVar

int(name, lb, ub)#

Create a ladder-encoded bounded integer variable over domain [lb, ub].

Parameters:

name (str)
lb (int)
ub (int)

Return type:

IntVar

int_set(name, *, lb=None, ub=None, values=None)#

Create an integer set variable over a finite universe.

Exactly one domain specification must be provided:

lb/ub inclusive range
explicit values sequence

Parameters:

name (str)
lb (int | None)
ub (int | None)
values (Sequence[int] | None)

Return type:

IntSetVar

floor_div(x, divisor, name=None)#

Materialize a quotient integer x // divisor using ladder threshold ties.

Parameters:

x (IntVar | _LazyIntExpr)
divisor (int)
name (str | None)

Return type:

IntVar

scale(x, factor, name=None)#

Materialize a scaled integer x * factor using ladder threshold ties.

Parameters:

x (IntVar | _LazyIntExpr)
factor (int)
name (str | None)

Return type:

IntVar

max(vec_or_items, name=None)#

Materialize exact maximum over an IntVector or IntVar sequence.

Parameters:: name (str | None)
Return type:: IntVar

min(vec_or_items, name=None)#

Materialize exact minimum over an IntVector or IntVar sequence.

Parameters:: name (str | None)
Return type:: IntVar

upper_bound(vec_or_items, name=None)#

Materialize one-sided aggregate constrained to be >= all vector items.

Parameters:: name (str | None)
Return type:: IntVar

lower_bound(vec_or_items, name=None)#

Materialize one-sided aggregate constrained to be <= all vector items.

Parameters:: name (str | None)
Return type:: IntVar

bool_vector(name, length)#

Create a vector of Boolean literals.

Parameters:

name (str)
length (int)

Return type:

BoolVector

int_vector(name, length, lb, ub)#

Create a vector of bounded integers sharing the same domain.

Parameters:

name (str)
length (int)
lb (int)
ub (int)

Return type:

IntVector

enum_vector(name, length, choices, nullable=False)#

Create a vector of enum variables.

Parameters:

name (str)
length (int)
choices (Sequence[str])
nullable (bool)

Return type:

EnumVector

int_set_vector(name, length, *, lb=None, ub=None, values=None)#

Create a vector of integer set variables with shared universe specification.

Parameters:

name (str)
length (int)
lb (int | None)
ub (int | None)
values (Sequence[int] | None)

Return type:

IntSetVector

bool_dict(name, keys)#

Create a keyed dictionary of Boolean literals.

Parameters:

name (str)
keys (Sequence)

Return type:

BoolDict

int_dict(name, keys, lb, ub)#

Create a keyed dictionary of bounded integers.

Parameters:

name (str)
keys (Sequence)
lb (int)
ub (int)

Return type:

IntDict

enum_dict(name, keys, choices, nullable=False)#

Create a keyed dictionary of enum variables.

Parameters:

name (str)
keys (Sequence)
choices (Sequence[str])
nullable (bool)

Return type:

EnumDict

int_set_dict(name, keys, *, lb=None, ub=None, values=None)#

Create a keyed dictionary of integer set variables.

Parameters:

name (str)
keys (Sequence)
lb (int | None)
ub (int | None)
values (Sequence[int] | None)

Return type:

IntSetDict

int_matrix(name, rows, cols, lb, ub)#

Create an integer matrix.

Parameters:

name (str)
rows (int)
cols (int)
lb (int)
ub (int)

Return type:

IntMatrix

interval(name, *, start, duration, end)#

Create a fixed-duration interval with inclusive latest-end horizon.

Parameters:

name (str) – User-facing interval identifier.
start (int) – Earliest start time (inclusive).
duration (int) – Positive fixed duration.
end (int) – Latest end time (inclusive).

Return type:

IntervalVar

sum_var(items, name=None)#

Materialize the sum of integer variables as a single IntVar.

Uses a binary-tree reduction: repeatedly merge the two narrowest current partial sums. This keeps intermediate widths smaller than a left-fold or, while avoiding the O(N) linear chain.

Parameters:

items (Sequence[IntVar])
name (str | None)

Return type:

IntVar

cumulative(starts, durations, demands, capacity, *, backend='auto')#

Add a fixed-duration cumulative resource constraint.

This is an interval scheduling primitive over explicit start variables and constant durations/demands.

Parameters:

backend (str) –
Encoding strategy for capacity cuts.

"time" loops over every integer time tick in the horizon and adds a PB capacity constraint at each. Formula size is O(N × H) where H is the horizon width. Efficient when task count N is very large relative to H.

"task" creates O(N²) pairwise precedence indicator variables (one per conflicting pair), then conditionally adds capacity cuts only at the start-times of active tasks. Formula size is O(N² × N). Efficient when H is large and N is small.

"auto" (default) picks "task" when N² < H, otherwise "time".
starts (Sequence[IntVar])
durations (Sequence[int])
demands (Sequence[int])
capacity (int)

Return type:

None

bool_matrix(name, rows, cols)#

Create a Boolean matrix.

Parameters:

name (str)
rows (int)
cols (int)

Return type:

BoolMatrix

enum_matrix(name, rows, cols, choices, nullable=False)#

Create an enum matrix.

Parameters:

name (str)
rows (int)
cols (int)
choices (Sequence[str])
nullable (bool)

Return type:

EnumMatrix

vector(items, name='_view')#

Build a typed vector view from a homogeneous sequence of model objects.

This is useful for arbitrary subsets (for example, Sudoku subgrids) that are not contiguous rows/columns.

Parameters:

items (Sequence)
name (str)

close_incremental()#

Close any bound incremental backend for this model.

Return type:: None

add_soft(constraint, weight)#

Compatibility alias for Model.obj.add_soft().

Parameters:: weight (int)

update_soft_weight(target, new_weight)#

Compatibility alias for Model.obj.update_soft().

Parameters:: new_weight (int)
Return type:: None

to_cnf()#

Export the current hard constraints to a PySAT CNF.

Raises:: ValueError – If the model contains soft clauses.
Return type:: CNF

to_wcnf()#

Export hard and soft constraints to a PySAT WCNF.

Return type:: WCNF

decode_model(model_lits)#

Return a decoded assignment view for a raw solver model.

Parameters:: model_lits (Sequence[int])
Return type:: AssignmentView

solve(*, sat_solver_name='g4', maxsat_backend='rc2', solver=None, solver_kwargs=None, assumptions=None, incremental=True, backend='auto', raise_on_abnormal=False, sat_upgrade='upgrade', lex_strategy=None, time_limit=None)#

Solve the model using built-in convenience backends.

Behavior:

hard-only model -> PySAT SAT solver (sat_solver_name)
model with soft clauses -> PySAT RC2 (maxsat_backend='rc2')
if solver is provided, use a Hermax IPAMIRSolver class (or instance) with the model exported as WCNF (one-shot solve)

Notes

Assumptions accept int DIMACS literals, Literal, or unit Term with coefficient +1/-1; plain bool values are rejected. In incremental mode, SAT binding can upgrade to MaxSAT when soft clauses appear (controlled by sat_upgrade). lex_strategy is meaningful only when model.tier_obj is active.

Parameters:

sat_solver_name (str)
maxsat_backend (str)
solver_kwargs (dict | None)
assumptions (Sequence[object] | None)
incremental (bool)
backend (str)
raise_on_abnormal (bool)
sat_upgrade (str)
lex_strategy (str | None)
time_limit (float | None)

Return type:

SolveResult

class hermax.model.Literal#

Boolean literal bound to a Model variable id and polarity.

__init__(model, id_, name, polarity=True)#

Parameters:

model (Model)
id_ (int)
name (str)
polarity (bool)

id#

name#

polarity#

only_if(condition)#

Return a gated unit clause enforcing this literal only if condition is true.

Parameters:: condition (Literal)
Return type:: Clause

implies(target)#

Return encoding of self -> target.

Supported targets include Literal, Clause, ClauseGroup, and lazy PBConstraint.

class hermax.model.Clause#

Single CNF clause (disjunction of literals).

__init__(model, literals)#

Parameters:

model (Model)
literals (Sequence['Literal'])

classmethod from_dimacs(model, ints)#

Parameters:

model (Model)
ints (Sequence[int])

Return type:

Clause

property literals: list[Literal]#

property dimacs: tuple[int, ...]#

classmethod from_iterable(literals)#

Build a clause from an iterable of literals.

Raises:

ValueError – If the iterable is empty.
ValueError – If literals belong to different models.

Parameters:

literals (Iterable[Literal])

Return type:

Clause

append(literal, *, inplace=False)#

Append a literal to this clause when inplace=True.

Warning

Mutation requires inplace=True. Prefer clause | lit (or clause |= lit with rebinding) for immutable operator behavior.

Parameters:

literal (Literal)
inplace (bool)

Return type:

Clause

only_if(condition)#

Return a gated clause enforcing this clause only when condition is true.

Meaning: condition -> clause.

Parameters:: condition (Literal)
Return type:: Clause

implies(target)#

Return CNF encoding of self -> target.

Clause implication is distributed over source literals: (a | b) -> X becomes (a -> X) & (b -> X).

class hermax.model.ClauseGroup#

Immutable collection of CNF clauses stored in DIMACS form.

__init__(model, clauses=None, *, amo_groups=None, eo_groups=None, reserve_aux_ids=True)#

Parameters:

model (Model)
clauses (Sequence['Clause | Sequence[int]'] | None)
amo_groups (Sequence[Sequence[int]] | None)
eo_groups (Sequence[Sequence[int]] | None)
reserve_aux_ids (bool)

is_empty()#

Return type:: bool

single_clause_or_none()#

Return type:: tuple[int, …] | None

iter_dimacs()#

materialize_semantic()#

Return type:: tuple[Clause, …]

only_if(condition)#

Return a new clause group gated by one literal.

Parameters:: condition (Literal)
Return type:: ClauseGroup

implies(target)#: Reject ClauseGroup-as-condition usage in this modeling API.

extend(other, *, inplace=False)#

Append/merge clauses into this clause group when inplace=True.

Supported inputs:: Literal, Clause, or ClauseGroup.

Warning

Mutation requires inplace=True. Prefer group & x (or group &= x with rebinding) for immutable operator behavior.

Parameters:: inplace (bool)
Return type:: ClauseGroup

class hermax.model.SoftRef#

Reference handle returned by Model.obj.add_soft().

__init__(group_id, soft_ids)#

Parameters:

group_id (int)
soft_ids (Sequence[int])

group_id#

soft_ids#

PB Layer#

class hermax.model.Term#

Weighted literal term used inside PBExpr.

coefficient: int | float#

literal: Literal#

__init__(coefficient, literal)#

Parameters:

coefficient (int | float)
literal (Literal)

Return type:

None

class hermax.model.PBExpr#

Pseudo-Boolean expression (weighted sum of literals / lifted Int variables).

__init__(model, terms=None, constant=0, int_terms=None)#

Parameters:

model (Model)
terms (Sequence[Term] | None)
constant (int)
int_terms (Sequence[tuple[int, IntVar | _LazyIntExpr]] | None)

terms#

constant#

int_terms#

classmethod from_item(item)#

Convert a supported item into a PBExpr.

Supported inputs: PBExpr, Term, Literal, IntVar, and integer constants.

Return type:: PBExpr

add(other, *, inplace=False)#

Add a PB-compatible item to this expression when inplace=True.

Warning

Mutation requires inplace=True. Prefer expr + x (or expr += x with rebinding) for immutable operator behavior.

Parameters:: inplace (bool)
Return type:: PBExpr

sub(other, *, inplace=False)#

Subtract a PB-compatible item from this expression when inplace=True.

Warning

Mutation requires inplace=True. Prefer expr - x (or expr -= x with rebinding) for immutable operator behavior.

Parameters:: inplace (bool)
Return type:: PBExpr

class hermax.model.PBConstraint#

Immutable lazy PB comparator descriptor compiled on demand.

Instances are produced by comparing PBExpr objects (or compatible operands) and preserve comparator metadata until compilation.

__init__(model, lhs, op, rhs, conditions=None)#

Parameters:

model (Model)
lhs (PBExpr)
op (str)
rhs (PBExpr)
conditions (Sequence[Literal] | None)

only_if(condition)#

Return a new PB constraint gated by a literal.

Meaning: condition -> PB.

Parameters:: condition (Literal)
Return type:: PBConstraint

implies(target)#

Return encoding of PB -> literal for the supported safe subset.

The target must be a Literal. The implementation uses safe contrapositive rewrites (and a selector split for equality antecedents).

clauses()#

Compile to a ClauseGroup and cache the result.

Return type:: ClauseGroup

class hermax.model.DivExpr#

Lazy IntVar // constant derived integer expression.

__init__(src, divisor)#

Parameters:

src (IntVar | _LazyIntExpr)
divisor (int)

property lb: int#: Lower bound of this lazy quotient expression.

property ub: int#: Upper bound of this lazy quotient expression.

class hermax.model.MaxExpr#

Lazy vector aggregate/bound derived integer expression.

__init__(model, items, kind, name=None)#

Parameters:

model (Model)
items (Sequence['IntVar'])
kind (str)
name (Optional[str])

property lb: int#: Lower bound of this lazy aggregate expression.

property ub: int#: Upper bound of this lazy aggregate expression.

Typed Variables#

class hermax.model.EnumVar#

Finite-domain categorical variable encoded as choice literals.

__init__(model, name, choices, nullable)#

Parameters:

model (Model)
name (str)
choices (Sequence[str])
nullable (bool)

name#

choices#

nullable#

is_in(choices)#

Return a CNF clause asserting the enum is one of choices.

This is a fast subset-disjunction helper that directly reuses the underlying choice literals and introduces no auxiliary variables.

Parameters:: choices (Sequence[str]) – Sequence of allowed enum labels.
Returns:: A Clause equivalent to (self == c1) | (self == c2) | ....
Raises:: ValueError – If choices is empty or contains an unknown label.
Return type:: Clause

is_in_or_none(choices)#

Return a nullable subset-membership constraint including None.

This helper is only valid for nullable enums and encodes membership in set(choices) ∪ {None} by forbidding all excluded concrete labels. It introduces no auxiliary variables but may require multiple clauses.

Parameters:: choices (Sequence[str]) – Allowed concrete enum labels. The nullable None branch is always allowed by this method.
Returns:: A ClauseGroup encoding membership in choices or None.
Raises:: ValueError – If the enum is non-nullable, if choices contains an unknown label, or if choices is empty.
Return type:: ClauseGroup

class hermax.model.IntVar#

Bounded integer variable with ladder/order encoding.

Domain are [lb, ub] (upper bound included).

__init__(model, name, lb, ub)#

Parameters:

model (Model)
name (str)
lb (int)
ub (int)

name#

lb#

ub#

lower_bound()#

Return the current static lower bound of the integer domain.

The modeling layer uses closed domains [lb, ub], so this returns lb exactly.

Return type:: int

upper_bound()#

Return the current static upper bound (inclusive) of the integer domain.

Return type:: int

scale(factor)#

Return a lazy derived integer expression for self * factor.

This is the lazy/holding-tank counterpart of Model.scale().

Parameters:: factor (int)

piecewise(*, base_value, steps)#

Return a lazy PB expression for a step function of this integer variable.

steps maps thresholds to the new function value active for all assignments self >= threshold.

Example

x.piecewise(base_value=10, steps={10: 25, 50: 100})

The returned object is a PBExpr and burns no new variables or clauses at construction time. Negative deltas are handled by the normal PB normalization pipeline when the expression is later constrained.

Parameters:

base_value (int)
steps (Mapping[int, int])

Return type:

PBExpr

forbid_value(value)#

Return a clause forbidding a single value from the domain.

This exploits the ladder “cliff” representation of exact values and compiles to a tiny clause (typically binary, unit on boundaries).

Parameters:: value (int)
Return type:: Clause

forbid_interval(start, end)#

Return a clause forbidding all values in the closed interval [start, end].

The interval is clipped to the declared integer domain. The resulting clause is typically binary, but can collapse to a unit clause, a tautology, or a contradiction at boundaries.

Parameters:

start (int)
end (int)

Return type:

Clause

in_range(start, end)#

Return a lazy indicator literal for inclusive membership start <= x <= end.

The returned literal is safe to construct and discard: any helper clauses defining the indicator are registered lazily and only materialized when the literal is consumed by a model sink/export.

Parameters:

start (int)
end (int)

Return type:

Literal

distance_at_most(other, max_distance)#

Return a constraint enforcing |self - other| <= max_distance.

This uses ladder-native implications and introduces no auxiliary variables.

Parameters:

other (IntVar)
max_distance (int)

Return type:

ClauseGroup

class hermax.model.IntervalVar#

Fixed-duration interval variable for scheduling-style constraints.

The constructor binds two IntVar objects, start and end, and enforces end == start + duration. Public horizon is:

start argument = earliest start (inclusive)
end argument = latest end (inclusive)

__init__(model, name, *, start, duration, end)#

Parameters:

model (Model)
name (str)
start (int)
duration (int)
end (int)

name#

duration#

earliest_start#

latest_end#

start#

end#

ends_before(other)#

Return constraint enforcing self.end <= other.start.

Parameters:: other (IntervalVar)
Return type:: ClauseGroup

starts_after(other)#

Return constraint enforcing self.start >= other.end.

Parameters:: other (IntervalVar)
Return type:: ClauseGroup

no_overlap(other)#

Return disjunctive non-overlap: self before other OR vice versa.

Parameters:: other (IntervalVar)
Return type:: ClauseGroup

Collections#

class hermax.model.BoolVector#

Vector of Boolean literals.

at_most_one()#: Return a cardinality constraint enforcing at most one true literal.

exactly_one()#: Return a cardinality constraint enforcing exactly one true literal.

at_least_one()#: Return a single clause enforcing at least one true literal.

name#

class hermax.model.EnumVector#

Vector of EnumVar values.

all_different(backend='auto')#

Return an all-different constraint over all enum elements.

Backends:: auto (default): column-wise AMO over enum choice literals. bipartite: same as auto (or pairwise fallback for nullable enums). pairwise: pairwise enum inequality constraints.

Parameters:: backend (str)
Return type:: ClauseGroup

name#

class hermax.model.IntVector#

Vector of IntVar values with common global helpers.

max(name=None)#

Create and return an IntVar equal to the maximum of the vector.

This is encoded directly on ladder threshold bits (bitwise OR across x >= k predicates), avoiding PB/cardinality encoders.

Parameters:: name (str | None)

min(name=None)#

Create and return an IntVar equal to the minimum of the vector.

This is encoded directly on ladder threshold bits (bitwise AND across x >= k predicates), avoiding PB/cardinality encoders.

Parameters:: name (str | None)

upper_bound(name=None)#

Create an IntVar constrained to be >= every element in the vector.

This is a one-sided aggregate (not exact max) and is cheaper than max() because it only emits upward-pressure clauses.

Parameters:: name (str | None)

lower_bound(name=None)#

Create an IntVar constrained to be <= every element in the vector.

This is a one-sided aggregate (not exact min) and is cheaper than min() because it only emits downward-pressure clauses.

Parameters:: name (str | None)

running_max(name=None)#

Return prefix maxima as a materialized IntVector.

out[i] equals max(self[:i+1]). This uses a cumulative fold with Model.max() to avoid the common O(N^2) prefix-max modeling trap of recomputing max(self[:i]) independently at each step.

Parameters:: name (str | None)
Return type:: IntVector

running_min(name=None)#

Return prefix minima as a materialized IntVector.

out[i] equals min(self[:i+1]) using the same cumulative-fold construction pattern as running_max().

Parameters:: name (str | None)
Return type:: IntVector

running_sum(name=None)#

Return prefix sums as a materialized IntVector.

out[i] equals sum(self[:i+1]). This is built as a cumulative fold with one fresh integer variable per prefix step, avoiding repeated re-materialization of larger and larger PB expressions.

Parameters:: name (str | None)
Return type:: IntVector

all_different(backend='auto')#

Return an all-different constraint over all integer elements.

Backends:: auto (default): currently aliases to pairwise. pairwise: pairwise integer inequality constraints. bipartite: channel to exact-value indicators + column AMOs.

Parameters:: backend (str)
Return type:: ClauseGroup

increasing()#

Return nondecreasing chain constraints x[i] <= x[i+1].

Return type:: ClauseGroup

lexicographic_less_than(other)#

Return strict lexicographic ordering constraint self <lex other.

Parameters:: other (IntVector)
Return type:: ClauseGroup

name#

class hermax.model.BoolDict#

Keyed mapping from user keys to Boolean literals.

name#

class hermax.model.EnumDict#

Keyed mapping from user keys to EnumVar values.

name#

class hermax.model.IntDict#

Keyed mapping from user keys to IntVar values.

name#

class hermax.model.BoolMatrix#

Dense matrix of Boolean literals.

__init__(model, name, rows, cols)#

Parameters:

model (Model)
name (str)
rows (int)
cols (int)

name#

row(r)#

Return row r as a BoolVector.

Parameters:: r (int)
Return type:: BoolVector

col(c)#

Return column c as a BoolVector.

Parameters:: c (int)
Return type:: BoolVector

flatten()#

Return all cells in row-major order as a BoolVector.

Return type:: BoolVector

class hermax.model.EnumMatrix#

Dense matrix of EnumVar cells.

__init__(model, name, rows, cols, choices, nullable=False)#

Parameters:

model (Model)
name (str)
rows (int)
cols (int)
choices (Sequence[str])
nullable (bool)

name#

row(r)#

Return row r as an EnumVector.

Parameters:: r (int)
Return type:: EnumVector

col(c)#

Return column c as an EnumVector.

Parameters:: c (int)
Return type:: EnumVector

flatten()#

Return all cells in row-major order as an EnumVector.

Return type:: EnumVector

class hermax.model.IntMatrix#

Dense matrix of IntVar cells.

__init__(model, name, rows, cols, lb, ub)#

Parameters:

model (Model)
name (str)
rows (int)
cols (int)
lb (int)
ub (int)

name#

row(r)#

Return row r as an IntVector.

Parameters:: r (int)
Return type:: IntVector

col(c)#

Return column c as an IntVector.

Parameters:: c (int)
Return type:: IntVector

flatten()#

Return all cells in row-major order as an IntVector.

Return type:: IntVector

Decode / Solve Results#

class hermax.model.AssignmentView#

Decoded view over a raw SAT/MaxSAT model for a specific Model.

__init__(model, raw_model)#

Parameters:

model (Model)
raw_model (Sequence[int])

property raw: list[int]#: Return a copy of the raw solver model literals.

val(obj)#

Decode the value of a model-bound object from the current assignment.

Parameters:: obj (Any) – The object to decode. Supported types include: - Literal: returns a bool. - IntVar: returns an int. - EnumVar: returns the chosen str (or None if nullable). - IntSetVar: returns a set[int]. - IntervalVar: returns a dict with start, end, and duration. - IntVector, BoolVector, etc.: returns a list of decoded values. - IntMatrix, BoolMatrix, etc.: returns a nested list (rows/cols). - IntDict, BoolDict, etc.: returns a dict with decoded values. - Nested list or tuple of supported objects.
Returns:: The Python-native value representing the variable’s state in this model.
Raises:: TypeError – if obj is not a supported target for decoding.
Return type:: Any

class hermax.model.SolveResult#

Convenience result object returned by Model.solve().

__init__(model, *, status, raw_model, cost, backend, tier_costs=None, tier_models=None)#

Parameters:

model (Model)
status (str)
raw_model (Sequence[int] | None)
cost (int | float | None)
backend (str)
tier_costs (list[int | float] | None)
tier_models (list[list[int]] | None)

status#

raw_model#

cost#

backend#

assignment#

tier_costs#

tier_models#

property ok: bool#: Return True when a feasible assignment is available.