Solver Interface#
List of Classes and Helpers#
Solver status codes, aligned with IPAMIR C API. |
|
Abstract Base Class for IPAMIR-compatible solvers. |
|
Returns True if the status code indicates a feasible solution was found. |
|
Returns True if the status code indicates the search was definitive (UNSAT or OPTIMUM). |
Module Description#
This module defines the Python contract implemented by Hermax
solvers through hermax.core.ipamir_solver_interface.IPAMIRSolver.
The contract is an adaptation of the incremental MaxSAT interface proposed by
IPAMIR [1] and rooted in the assumption-based incremental SAT model [2] [3].
At a high level, the interface separates:
hard constraints via
add_clauseoptimization terms via
set_soft/add_soft_unit/add_soft_relaxedper-call assumptions via
solve(assumptions=...)result/status introspection via
get_status,get_cost, andget_model
This explicit split is important for incremental MaxSAT, where assumptions and weight updates can vary between calls while preserving part of the solver state and learned information [1] [4] [5].
Status#
hermax.core.ipamir_solver_interface.SolveStatus follows IPAMIR
status codes and distinguishes three categories:
feasible but not necessarily optimal (
INTERRUPTED_SAT)final (
UNSATandOPTIMUM)abnormal/intermediate states (
INTERRUPTED,ERROR,UNKNOWN)
Use hermax.core.ipamir_solver_interface.is_feasible() and
hermax.core.ipamir_solver_interface.is_final() to write backend-agnostic
control flow over multiple solvers.
IPAMIRSolver API Details#
- class hermax.core.ipamir_solver_interface.IPAMIRSolver#
Bases:
ABCAbstract Base Class for IPAMIR-compatible solvers.
This interface is a Pythonic adaptation of the IPAMIR (Incremental Parameterizable MaxSAT Interface) C API. It defines the core methods required for incremental MaxSAT solving, including:
adding hard clauses (add_clause)
defining/updating soft literals (set_soft, add_soft_unit)
solving under temporary assumptions (solve(assumptions=…))
querying status/cost/model after each call
The interface intentionally exposes solver-agnostic primitives; different concrete backends may implement different internal state reuse policies while preserving this external contract.
- __init__(*args, **kwargs)#
- abstractmethod 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
- abstractmethod 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
- abstractmethod 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)
- abstractmethod 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
- abstractmethod get_status()#
Return last solver status.
- Return type:
- abstractmethod get_cost()#
Objective value of the last solution. Raises RuntimeError if status is not SAT or OPTIMUM.
- Return type:
int
- abstractmethod 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
- abstractmethod 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
- abstractmethod signature()#
Return solver signature string (name, version).
- Return type:
str
- abstractmethod close()#
Release underlying resources.
- Return type:
None
- new_var()#
Allocate a fresh variable id. Optional.
- Return type:
int
- set_terminate(callback)#
Register callback. Optional.
- Parameters:
callback (Callable[[], int] | None)
- Return type:
None
- set_callback(callback)#
Register a generic callback. Optional.
- Parameters:
callback (Callable[[], None] | None)
- Return type:
None
SolveStatus API Details#
Helper Functions#
- hermax.core.ipamir_solver_interface.is_feasible(st)#
Returns True if the status code indicates a feasible solution was found.
- Parameters:
st (SolveStatus)
- Return type:
bool
- hermax.core.ipamir_solver_interface.is_final(st)#
Returns True if the status code indicates the search was definitive (UNSAT or OPTIMUM).
- Parameters:
st (SolveStatus)
- Return type:
bool