Incremental Solvers

List of Classes

hermax.incremental.UWrMaxSAT	UWrMaxSAT: an efficient MaxSAT solver based on the UWrMaxSAT 1.8 solver.
hermax.incremental.UWrMaxSATCompetition	UWrMaxSAT (Competition version): A highly efficient MaxSAT solver, specifically the version 1.4 used in competitions.
hermax.incremental.EvalMaxSAT	EvalMaxSAT: Latest version of EvalMaxSAT with native IPAMIR support.
hermax.incremental.EvalMaxSATIncremental	EvalMaxSAT (Incremental): Specialized incremental version of EvalMaxSAT.
hermax.incremental.IMaxHS	iMaxHS: optional IPAMIR-style incremental solver backed by MaxHS+CPLEX.

Module Description

This module exposes Hermax classes backed by solvers that are used through an incremental/IPAMIR workflow, i.e., repeated solve calls while preserving internal state and/or interface state [1].

The classes map to the following backends:

• hermax.incremental.UWrMaxSAT: hermax.core.uwrmaxsat_py.UWrMaxSATSolver (UWrMaxSAT family [2]).

• hermax.incremental.UWrMaxSATCompetition: hermax.core.uwrmaxsat_comp_py.UWrMaxSATCompSolver (competition branch of UWrMaxSAT [2]).

• hermax.incremental.EvalMaxSAT: hermax.core.evalmaxsat_latest_py.EvalMaxSATLatestSolver (EvalMaxSAT family [3]).

• hermax.incremental.EvalMaxSATIncremental: hermax.core.evalmaxsat_incr_py.EvalMaxSATIncrSolver (incremental EvalMaxSAT backend [3]).

• hermax.incremental.IMaxHS: hermax.core.imaxhs_wrapper_py.IMaxHSSolver (optional CPLEX-backed iMaxHS backend [4]).

Warning

In Hermax package builds, both UWrMaxSAT and UWrMaxSATCompetition are compiled with SCIP integration disabled.

Warning

On Windows and macOS, preprocessing is disabled for UWrMaxSATCompetition due to upstream undefined behavior (UB) that can cause native crashes.

Warning

On macOS, preprocessing is disabled for EvalMaxSAT backends due to possible native crashes.

Incremental MaxSAT

Incremental MaxSAT behavior differs substantially across solver families [1]:

• UWrMaxSAT is a trutly incremental MaxSAT solver based on PB optimization [2].

• EvalMaxSAT uses an copy and re-solve strategy [3].

API Details

class hermax.incremental.UWrMaxSAT

Bases: UWrMaxSATSolver

UWrMaxSAT: an efficient MaxSAT solver based on the UWrMaxSAT 1.8 solver. This solver provides native incremental support through the IPAMIR interface.

UWrMaxSAT is known for its efficiency in handling various MaxSAT instances, combining modern SAT solving techniques with effective MaxSAT algorithms.

Note

Hermax package builds compile UWrMaxSAT with SCIP integration disabled.

__init__(formula=None, *args, **kwargs)

Parameters:

formula (WCNF | None)

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

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)

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

close()

Release underlying resources.

Return type:

None

get_cost()

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

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

get_status()

Return last solver status.

Return type:

SolveStatus

new_var()

Allocate a fresh variable id. Optional.

Return type:

int

set_callback(callback)

Register a generic callback. Optional.

Parameters:

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

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

set_terminate(callback)

Register callback. Optional.

Parameters:

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

Return type:

None

signature()

Return solver signature string (name, version).

Return type:

str

solve(assumptions=None, raise_on_abnormal=False)

Solve the formula under the given assumptions.

Parameters:

• assumptions – A list of literals to be used as assumptions for this solve call. These are cleared after the solve.

• raise_on_abnormal – 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

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

class hermax.incremental.UWrMaxSATCompetition

Bases: UWrMaxSATCompSolver

UWrMaxSAT (Competition version): A highly efficient MaxSAT solver, specifically the version 1.4 used in competitions. This solver provides native incremental support through the IPAMIR interface.

It is particularly optimized for competition-style benchmarks and provides robust performance across a wide range of MaxSAT problems.

Note

Hermax package builds compile UWrMaxSATCompetition with SCIP integration disabled.

__init__(formula=None, *args, **kwargs)

Parameters:

formula (WCNF | None)

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

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)

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

close()

Release underlying resources.

Return type:

None

get_cost()

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

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

get_status()

Return last solver status.

Return type:

SolveStatus

new_var()

Allocate a fresh variable id. Optional.

Return type:

int

set_callback(callback)

Register a generic callback. Optional.

Parameters:

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

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

set_terminate(callback)

Register callback. Optional.

Parameters:

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

Return type:

None

signature()

Return solver signature string (name, version).

Return type:

str

solve(assumptions=None, raise_on_abnormal=False)

Solve the formula under the given assumptions.

Parameters:

• assumptions – A list of literals to be used as assumptions for this solve call. These are cleared after the solve.

• raise_on_abnormal – 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

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

class hermax.incremental.EvalMaxSAT

Bases: EvalMaxSATLatestSolver

EvalMaxSAT: Latest version of EvalMaxSAT with native IPAMIR support.

EvalMaxSAT is a state-of-the-art solver known for its performance in MaxSAT competitions.

__init__(formula=None, *args, **kwargs)

Parameters:

formula (WCNF | None)

add_clause(clause, weight=None)

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])

• weight (int | None)

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)

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

close()

Release underlying resources.

Return type:

None

get_cost()

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

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

get_status()

Return last solver status.

Return type:

SolveStatus

new_var()

Allocate a fresh variable id. Optional.

Return type:

int

nonunit_soft_policy: str = 'relax'

set_callback(callback)

Register a generic callback. Optional.

Parameters:

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

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

set_terminate(callback)

Register callback. Optional.

Parameters:

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

Return type:

None

signature()

Return solver signature string (name, version).

Return type:

str

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

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

class hermax.incremental.EvalMaxSATIncremental

Bases: EvalMaxSATIncrSolver

EvalMaxSAT (Incremental): Specialized incremental version of EvalMaxSAT.

__init__(formula=None, *args, **kwargs)

Parameters:

formula (WCNF | None)

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

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)

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

close()

Release underlying resources.

Return type:

None

get_cost()

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

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

get_status()

Return last solver status.

Return type:

SolveStatus

new_var()

Allocate a fresh variable id. Optional.

Return type:

int

set_callback(callback)

Register a generic callback. Optional.

Parameters:

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

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

set_terminate(callback)

Register callback. Optional.

Parameters:

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

Return type:

None

signature()

Return solver signature string (name, version).

Return type:

str

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

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

class hermax.incremental.IMaxHS

Bases: IMaxHSSolver

iMaxHS: optional IPAMIR-style incremental solver backed by MaxHS+CPLEX.

Notes

This backend is only available when Hermax is compiled with CPLEX headers/libraries present.

__init__(formula=None, *args, **kwargs)

Parameters:

formula (WCNF | None)

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

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)

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

close()

Release underlying resources.

Return type:

None

get_cost()

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

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

get_status()

Return last solver status.

Return type:

SolveStatus

classmethod is_available()

Return type:

bool

new_var()

Allocate a fresh variable id. Optional.

Return type:

int

set_callback(callback)

Register a generic callback. Optional.

Parameters:

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

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

set_terminate(callback)

Register callback. Optional.

Parameters:

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

Return type:

None

signature()

Return solver signature string (name, version).

Return type:

str

solve(assumptions=None, raise_on_abnormal=False)

Solve the formula under the given assumptions.

Parameters:

• assumptions – A list of literals to be used as assumptions for this solve call. These are cleared after the solve.

• raise_on_abnormal – 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

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

References

[1] (1,2)

Andreas Niskanen, Jeremias Berg, Matti Järvisalo. Incremental Maximum Satisfiability. SAT 2022.

[2] (1,2,3)

Marek Piotrów. UWrMaxSat: Efficient Solver for MaxSAT and Pseudo-Boolean Problems. ICTAI 2020.

[3] (1,2,3)

Florent Avellaneda. EvalMaxSAT. MaxSAT Evaluation: Solver and Benchmark Descriptions, 2023.

[4]

Andreas Niskanen, Jeremias Berg, Matti Järvisalo. Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights. CP 2021.