Portfolio Solver#

The hermax.portfolio package provides a process-isolated solver portfolio that can race multiple Hermax solver classes on the same MaxSAT instance.

Unlike the incomplete-solver wrappers, the portfolio is a general front-end: it accepts incremental wrappers, non-incremental wrappers, and incomplete solvers in the same run. Each solver is executed in its own subprocess for robustness and timeout control.

Module Description#

Warning

The portfolio module is experimental/beta and may be subject to significant interface changes.

PortfolioSolver is a fake-incremental wrapper:

  • it caches the formula in Python

  • records an IPAMIR-level operation log

  • replays that log into fresh worker processes on each solve()

  • validates returned models/costs (enabled by default)

  • selects a final result according to a configurable policy

Users pass Python classes for example:

from hermax.portfolio import PortfolioSolver
from hermax.non_incremental import CGSSSolver
from hermax.non_incremental.incomplete import Loandra, OpenWBOInc, TTOpenWBOInc

s = PortfolioSolver(
    [CGSSSolver, Loandra, OpenWBOInc, TTOpenWBOInc],
    per_solver_timeout_s=5.0,
    overall_timeout_s=10.0,
    selection_policy="first_optimal_or_best_until_timeout",
)

Preset Portfolios#

Hermax also provides auto-discovered preset portfolio subclasses:

These presets discover solver classes automatically from the public namespace structure:

  • CompletePortfolioSolver: hermax.incremental + hermax.non_incremental

  • IncompletePortfolioSolver: hermax.non_incremental.incomplete

  • PerformancePortfolioSolver: union of complete + incomplete namespaces

This discovery is structural and deterministic (no separate static registry is required). Presets:

  • use namespace __all__ exports as the membership contract

  • keep only classes implementing hermax.core.ipamir_solver_interface.IPAMIRSolver

  • skip abstract classes

  • de-duplicate aliases by the effective worker class used inside the subprocess (important for incomplete wrappers), and

  • sort deterministically by effective worker class path

Example (preset subclass):

from hermax.portfolio import PerformancePortfolioSolver

s = PerformancePortfolioSolver(
    per_solver_timeout_s=5.0,
    overall_timeout_s=15.0,
    max_workers=4,
)

Example (classmethod constructors):

from hermax.portfolio import PortfolioSolver

s1 = PortfolioSolver.complete(max_workers=4)
s2 = PortfolioSolver.incomplete(selection_policy="first_valid")
s3 = PortfolioSolver.performance(
    per_solver_timeout_s=5.0,
    overall_timeout_s=15.0,
    max_workers=8,
)

Key options#

  • selection_policy:

    • "best_valid_until_timeout"

    • "first_valid"

    • "first_optimal_or_best_until_timeout" (default)

  • max_workers (default 0 = no limit): maximum number of solver subprocesses run concurrently. This is a process concurrency limit (not an internal SAT/MaxSAT threading option).

  • validate_model (default True): reject results whose model violates hard clauses.

  • recompute_cost_from_model (default True): compute the portfolio cost from the returned model using Hermax/IPAMIR.

  • invalid_result_policy (default "warn_drop"): what to do with invalid solver outputs (warn/drop/raise/ignore).

Callback API#

PortfolioSolver supports event-driven callbacks through set_callback(...).

Supported callback signatures:

  • legacy: callback()

  • event form: callback(event)

If the callback raises an exception, the portfolio interprets it as STOP.

Events#

Callbacks receive hermax.portfolio.PortfolioEvent values:

  • event_type: "HEARTBEAT" or "INCUMBENT"

  • elapsed_s: time since solve() started

  • worker_id: worker index for incumbent events (None for heartbeat)

  • cost: incumbent cost (if available)

  • model: incumbent model list (if available)

  • is_optimal: whether incumbent status is optimal

Heartbeat cadence defaults to 1 second.

Incumbent callbacks are emitted on strict improvements only. If multiple improvements happen before callback dispatch, only the latest incumbent is sent.

Actions#

The callback may return:

AdjustTimeout supports:

  • mode="relative" (default): timeout from now

  • mode="absolute": timeout from solve start

Example#

from hermax.portfolio import (
    PortfolioSolver,
    PortfolioEvent,
    CallbackAction,
    AdjustTimeout,
)
from hermax.non_incremental import CGSSSolver
from hermax.non_incremental.incomplete import Loandra

def monitor(event: PortfolioEvent):
    if event.event_type == "HEARTBEAT":
        return
    if event.cost is not None and event.cost <= 50:
        return CallbackAction.STOP
    if event.cost is not None and event.cost <= 200:
        return AdjustTimeout(new_timeout_s=3.0, mode="relative")

s = PortfolioSolver([CGSSSolver, Loandra], overall_timeout_s=20.0)
s.set_callback(monitor)
s.solve()

Behavior Notes#

CompletePortfolioSolver and PerformancePortfolioSolver are suitable for IPAMIR conformance. IncompletePortfolioSolver is different by design:

  • it may return valid feasible solutions without proving optimality

  • it does not guarantee trusted UNSAT classification

  • it is therefore expected to use PASS/SKIP policies for exact-optimum and exact-UNSAT conformance tests.

API Details#

class hermax.portfolio.PortfolioSolver#

Bases: IPAMIRSolver

Portfolio MaxSAT solver that races multiple Hermax solver classes in parallel.

The portfolio is fake-incremental: it caches the formula in Python and replays an IPAMIR-level operation log into a fresh worker process per solver on each solve() call.

SUPPORTED_POLICIES = {'best_valid_until_timeout', 'first_optimal_or_best_until_timeout', 'first_valid'}#
CALLBACK_HEARTBEAT_S = 1.0#
__init__(solver_classes, formula=None, *, per_solver_timeout_s=20.0, overall_timeout_s=0.0, timeout_grace_s=1.0, max_workers=0, selection_policy='first_optimal_or_best_until_timeout', validate_model=True, recompute_cost_from_model=True, invalid_result_policy='warn_drop', verbose_invalid=True)#
Parameters:

  • solver_classes (Sequence[Type[IPAMIRSolver]])

  • per_solver_timeout_s (float)

  • overall_timeout_s (float)

  • timeout_grace_s (float)

  • max_workers (int)

  • selection_policy (str)

  • validate_model (bool)

  • recompute_cost_from_model (bool)

  • invalid_result_policy (str)

  • verbose_invalid (bool)

classmethod is_available()#
Return type:

bool

classmethod complete(*args, **kwargs)#
classmethod incomplete(*args, **kwargs)#
classmethod performance(*args, **kwargs)#
set_callback(callback)#

Register portfolio callback.

Compatible signatures: * callback() (legacy - deprecated) * callback(event: PortfolioEvent) (preferred)

Parameters:

callback (Callable[[...], Any] | None)

Return type:

None

new_var()#

Allocate a fresh variable id. Optional.

Return type:

int

add_clause(clause)#

Adds a hard clause to the solver.

A hard clause must be satisfied in every model. If an empty clause is added, the formula becomes UNSAT.

Example

solver.add_clause([-1, 2])

Parameters:

clause (list[int])

Return type:

None

set_soft(lit, weight)#

Declares or updates a soft literal.

A soft literal penalizes its positive assignment if the literal is negative (and vice versa). For example, set_soft(-1, 10) means variable 1 = True adds cost 10.

Example

solver.set_soft(-1, 5)

Parameters:

  • lit (int)

  • weight (int)

Return type:

None

add_soft_unit(lit, weight)#

Shortcut for add_soft_relaxed([lit], weight, relax_var=None).

Adds a soft unit clause. This is equivalent to:

  • adding a hard clause [lit]

  • associating a weight that penalizes its violation.

Example

solver.add_soft_unit(-1, 10)

Parameters:

  • lit (int)

  • weight (int)

Return type:

None

add_soft_relaxed(clause, weight, relax_var)#

Adds a non-unit soft clause, with explicit control over the relaxation variable.

  • clause is the list of literals in the base constraint.

  • weight is the cost if the clause is violated.

  • relax_var is the variable used to relax the clause:

    • If None and clause is unit, the solver automatically handles it.

    • If None and clause has more than one literal, this is invalid and must raise an error.

    • If given, the solver will add the hard clause (clause ∨ relax_var) and associate a soft unit clause (-relax_var) with the specified weight.

Example

# Non-unit soft clause: (-1 ∨ -2) with cost 5 and relaxation var 3 solver.add_soft_relaxed([-1, -2], 5, relax_var=3)

Parameters:

  • clause (list[int])

  • weight (int)

  • relax_var (int | None)

solve(assumptions=None, raise_on_abnormal=False)#

Solve the formula under the given assumptions.

Parameters:

  • assumptions (List[int] | None) – A list of literals to be used as assumptions for this solve call. These are cleared after the solve.

  • raise_on_abnormal (bool) – If True, raises a RuntimeError on status INTERRUPTED or ERROR.

Returns:

True if a feasible solution is found (status is SAT or OPTIMUM). False if the formula is UNSAT or the solve was interrupted without a solution.

Return type:

bool

get_status()#

Return last solver status.

Return type:

SolveStatus

get_cost()#

Objective value of the last solution. Raises RuntimeError if status is not SAT or OPTIMUM.

Return type:

int

val(lit)#

Return -1, 0, or +1 value of a literal in the last model.

  • -1: literal is false

  • 0: literal is unassigned/don’t care

  • +1: literal is true

Raises RuntimeError if no model is available.

Parameters:

lit (int)

Return type:

int

get_model()#

Return full model as a list of signed integers, or None. Raises RuntimeError if status is not SAT or OPTIMUM.

Return type:

List[int] | None

signature()#

Return solver signature string (name, version).

Return type:

str

close()#

Release underlying resources.

Return type:

None

property last_run_details: list[dict[str, Any]]#
set_terminate(callback)#

Register callback. Optional.

Parameters:

callback (Callable[[], int] | None)

Return type:

None

class hermax.portfolio.CompletePortfolioSolver#

Bases: _AutoPortfolioSolver

Auto-discovered portfolio over incremental + non-incremental (complete/reentrant) namespaces.

class hermax.portfolio.IncompletePortfolioSolver#

Bases: _AutoPortfolioSolver

Auto-discovered portfolio over incomplete subprocess-backed namespace.

class hermax.portfolio.PerformancePortfolioSolver#

Bases: _AutoPortfolioSolver

Auto-discovered mixed portfolio over complete + incomplete namespaces.

class hermax.portfolio.PortfolioEvent#

PortfolioEvent(event_type: ‘str’, elapsed_s: ‘float’, worker_id: ‘Optional[int]’ = None, cost: ‘Optional[int]’ = None, model: ‘Optional[List[int]]’ = None, is_optimal: ‘bool’ = False)

event_type: str#
elapsed_s: float#
worker_id: int | None = None#
cost: int | None = None#
model: List[int] | None = None#
is_optimal: bool = False#
__init__(event_type, elapsed_s, worker_id=None, cost=None, model=None, is_optimal=False)#
Parameters:

  • event_type (str)

  • elapsed_s (float)

  • worker_id (int | None)

  • cost (int | None)

  • model (List[int] | None)

  • is_optimal (bool)

Return type:

None

class hermax.portfolio.AdjustTimeout#

AdjustTimeout(new_timeout_s: ‘float’, mode: ‘str’ = ‘relative’)

new_timeout_s: float#
mode: str = 'relative'#
__init__(new_timeout_s, mode='relative')#
Parameters:

  • new_timeout_s (float)

  • mode (str)

Return type:

None

class hermax.portfolio.CallbackAction#
CONTINUE = 'CONTINUE'#
STOP = 'STOP'#
DROP_CURRENT = 'DROP_CURRENT'#