Non-Incremental Solvers

List of Classes

hermax.non_incremental.RC2	RC2: A powerful MaxSAT solver based on the RC2 algorithm, using the PySAT implementation.
hermax.non_incremental.UWrMaxSATCompetition	UWrMaxSAT (Competition version): A reentrant wrapper for the competition version 1.4.
hermax.non_incremental.EvalMaxSAT	EvalMaxSAT: Latest version of EvalMaxSAT, wrapped for reentrant incremental use.
hermax.non_incremental.MaxHS	MaxHS: optional re-encoding wrapper around the MaxHS backend.
hermax.non_incremental.CASHWMaxSAT	CASHWMaxSAT: An award-winning hybrid MaxSAT solver
hermax.non_incremental.CGSS	CGSS complete solver (RC2WCE + structure sharing + WCE), rebuild wrapper.
hermax.non_incremental.OpenWBOOLL	Open-WBO OLL algorithm (rebuild wrapper).
hermax.non_incremental.OpenWBOPartMSU3	Open-WBO PartMSU3 algorithm (rebuild wrapper).
hermax.non_incremental.OpenWBO	Open-WBO auto mode (rebuild wrapper): routes to OLL/PartMSU3/MSU3.

Module Description

This module groups wrappers and re-entrant adapters used when a backend is invoked in a non-native-incremental workflow, while exposing the common Hermax interface.

For incomplete / subprocess-isolated wrappers see Incomplete Non-Incremental Solvers and the developer note Solver Subprocess Isolation.

Backend mapping:

• hermax.non_incremental.RC2: hermax.core.rc2.RC2Reentrant (re-encoding wrapper around RC2 [1] [2] [8]).

• hermax.non_incremental.UWrMaxSATCompetition: hermax.core.uwrmaxsat_comp_py.UWrMaxSATCompReentrant [4].

• hermax.non_incremental.EvalMaxSAT: hermax.core.evalmaxsat_latest_py.EvalMaxSATLatestReentrant [5].

• hermax.non_incremental.MaxHS: hermax.core.maxhs_wrapper_py.MaxHSSolver (optional CPLEX-backed MaxHS wrapper [9]).

• hermax.non_incremental.CASHWMaxSAT: hermax.core.cashwmaxsat_py.CASHWMaxSATSolver [6].

• hermax.non_incremental.CGSS: hermax.core.cgss_py.CGSSSolver (RC2WCE/CGSS wrapper [7] [8]).

• hermax.non_incremental.OpenWBOOLL: hermax.core.openwbo_py.OLLSolver (Open-WBO OLL backend [8]).

• hermax.non_incremental.OpenWBOPartMSU3: hermax.core.openwbo_py.PartMSU3Solver (Open-WBO PartMSU3 backend [11] [12]).

• hermax.non_incremental.OpenWBO: hermax.core.openwbo_py.AutoOpenWBOSolver (Open-WBO auto routing: OLL/PartMSU3/MSU3).

Warning

In Hermax package builds, UWrMaxSATCompetition and CASHWMaxSAT is compiled with SCIP disabled.

Warning

Preprocessing is disabled for UWrMaxSATCompetition due to undefined behavior (UB) that can cause native crashes.

Warning

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

API Details

class hermax.non_incremental.RC2

Bases: RC2Reentrant

RC2: A powerful MaxSAT solver based on the RC2 algorithm, using the PySAT implementation. This version is reentrant and suitable for non-native incremental use.

__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 = 'store'

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.

Return type:

None

signature()

Return solver signature string (name, version).

Return type:

str

solve(assumptions=None, raise_on_abnormal=False, time_limit=None)

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.

• time_limit (float | None) – Optional finite positive wall-clock limit in seconds.

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.non_incremental.UWrMaxSATCompetition

Bases: UWrMaxSATCompReentrant

UWrMaxSAT (Competition version): A reentrant wrapper for the competition version 1.4.

Note

Hermax package builds compile this backend with SCIP integration disabled.

__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 = 'store'

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, time_limit=None)

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.

• time_limit (float | None) – Optional finite positive wall-clock limit in seconds.

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.non_incremental.EvalMaxSAT

Bases: EvalMaxSATLatestReentrant

EvalMaxSAT: Latest version of EvalMaxSAT, wrapped for reentrant incremental use.

__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 = 'store'

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.

Return type:

None

signature()

Return solver signature string (name, version).

Return type:

str

solve(assumptions=None, raise_on_abnormal=False, time_limit=None)

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.

• time_limit (float | None) – Optional finite positive wall-clock limit in seconds.

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.non_incremental.MaxHS

Bases: MaxHSSolver

MaxHS: optional re-encoding wrapper around the MaxHS backend.

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, 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

classmethod is_available()

Return type:

bool

new_var()

Allocate a fresh variable id. Optional.

Return type:

int

nonunit_soft_policy: str = 'store'

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.

Return type:

None

signature()

Return solver signature string (name, version).

Return type:

str

solve(assumptions=None, raise_on_abnormal=False, time_limit=None)

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.

• time_limit (float | None) – Optional finite positive wall-clock limit in seconds.

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.non_incremental.CASHWMaxSAT

Bases: CASHWMaxSATSolver

CASHWMaxSAT: An award-winning hybrid MaxSAT solver

Note

The wrapper defaults to disable_scip=True.

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

Parameters:

• formula (WCNF | None)

• disable_scip (bool)

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

disable_scip()

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, time_limit=None)

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.

• time_limit (float | None) – Optional finite positive wall-clock limit in seconds.

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.non_incremental.CGSS

Bases: CGSSSolver

CGSS complete solver (RC2WCE + structure sharing + WCE), rebuild wrapper.

__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

classmethod is_available()

Return type:

bool

new_var()

Allocate a fresh variable id. Optional.

Return type:

int

nonunit_soft_policy: str = 'store'

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, time_limit=None)

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.

• time_limit (float | None) – Optional finite positive wall-clock limit in seconds.

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.non_incremental.OpenWBOOLL

Bases: OLLSolver

Open-WBO OLL algorithm (rebuild wrapper).

__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, time_limit=None)

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.

• time_limit (float | None) – Optional finite positive wall-clock limit in seconds.

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.non_incremental.OpenWBOPartMSU3

Bases: PartMSU3Solver

Open-WBO PartMSU3 algorithm (rebuild wrapper).

__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, time_limit=None)

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.

• time_limit (float | None) – Optional finite positive wall-clock limit in seconds.

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.non_incremental.OpenWBO

Bases: AutoOpenWBOSolver

Open-WBO auto mode (rebuild wrapper): routes to OLL/PartMSU3/MSU3.

__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, time_limit=None)

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.

• time_limit (float | None) – Optional finite positive wall-clock limit in seconds.

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]

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva. RC2: An Efficient MaxSAT Solver. JSAT 11(1), 2019.

[2]

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva. PySAT: A Python Toolkit for Prototyping with SAT Oracles. SAT 2018.

[4]

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

[5]

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

[6]

Shiwei Pan, Yiyuan Wang, Shaowei Cai. An Efficient Core-Guided Solver for Weighted Partial MaxSAT. IJCAI 2025.

[7]

Hannes Ihalainen, Jeremias Berg, Matti Jarvisalo. Refined Core Relaxation for Core-Guided MaxSAT Solving. CP 2021.

[8] (1,2,3)

Benjamin Andres, Benjamin Kaufmann, Oliver Matheis, Torsten Schaub. Unsatisfiability-based Optimization in clasp. ICLP 2012 Technical Communications.

[9]

Jessica Davies, Fahiem Bacchus. Exploiting the power of MIP solvers in MAXSAT. International Conference on Theory and Applications of Satisfiability Testing, 2013.

[10]

Nina Narodytska, Fahiem Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. Proceedings of the AAAI Conference on Artificial Intelligence 28(1), 2014.

[11]

Antonio Morgado, Mark Liffiton, Joao Marques-Silva. MaxSAT-based MCS enumeration. Haifa Verification Conference, 2012.

[12]

Joao Marques-Silva, Jordi Planes. Algorithms for maximum satisfiability using unsatisfiable cores. Proceedings of the Conference on Design, Automation and Test in Europe, 2008.