Incomplete Non-Incremental Solvers

Documents the solvers in hermax.non_incremental.incomplete.

These solvers are:

• non-IPAMIR-native (they do not provide native incremental state reuse)

• incomplete (they may return a non optimal solution)

For this reason, callers should expect hermax.core.ipamir_solver_interface.SolveStatus values such as INTERRUPTED_SAT for valid but non-proven solutions.

Module Description

The hermax.non_incremental.incomplete namespace contains fake-incremental wrappers that cache the formula in Python and rebuild it on each solve(). Current implementations use subprocess isolation around native Python bindings to tolerate solver exit() behavior and provide robust timeouts.

Available classes

hermax.non_incremental.incomplete.OpenWBOInc	Open-WBO-Inc fake-incremental wrapper with one-shot subprocess isolation.
hermax.non_incremental.incomplete.TTOpenWBOInc	TT-Open-WBO-Inc fake-incremental wrapper with one-shot subprocess isolation.
hermax.non_incremental.incomplete.SPBMaxSATCFPS	SPB-MaxSAT-c-FPS fake-incremental wrapper with one-shot subprocess isolation.
hermax.non_incremental.incomplete.NuWLSCIBR	NuWLS-c-IBR fake-incremental wrapper with one-shot subprocess isolation.
hermax.non_incremental.incomplete.Loandra	Loandra fake-incremental wrapper with one-shot subprocess isolation.

Backend mapping

• hermax.non_incremental.incomplete.OpenWBOInc uses the native binding hermax.core.openwbo_inc and a subprocess-isolated wrapper in hermax.core.openwbo_inc_py.openwbo_inc_subprocess.

• hermax.non_incremental.incomplete.TTOpenWBOInc uses the native binding hermax.core.tt_openwbo_inc and a subprocess-isolated wrapper in hermax.core.tt_openwbo_inc_py.tt_openwbo_inc_subprocess.

• hermax.non_incremental.incomplete.SPBMaxSATCFPS uses the native binding hermax.core.spb_maxsat_c_fps and a subprocess-isolated wrapper in hermax.core.spb_maxsat_c_fps_py.spb_maxsat_c_fps_subprocess.

• hermax.non_incremental.incomplete.NuWLSCIBR uses the native binding hermax.core.nuwls_c_ibr and a subprocess-isolated wrapper in hermax.core.nuwls_c_ibr_py.nuwls_c_ibr_subprocess.

• hermax.non_incremental.incomplete.Loandra uses the native binding hermax.core.loandra and a subprocess-isolated wrapper in hermax.core.loandra_py.loandra_subprocess.

API Details

class hermax.non_incremental.incomplete.OpenWBOInc

Bases: OneShotSubprocessReplaySolverBase

Open-WBO-Inc fake-incremental wrapper with one-shot subprocess isolation.

pass_assumptions_to_worker: bool = False

nonunit_soft_policy: str = 'store'

property worker_solver_class_path: str

Import path to worker-side solver class.

property default_signature: str

Default wrapper signature label.

property timeout_error_prefix: str

Name used in timeout error message.

classmethod is_available()

Return type:

bool

__init__(formula=None, *args, default_time_limit=None, time_limit_grace=1.0, timeout_s=None, timeout_grace_s=None, **kwargs)

Parameters:

• formula (WCNF | None)

• default_time_limit (float | None)

• time_limit_grace (float)

• timeout_s (float | None)

• timeout_grace_s (float | 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

compat_exit_code_status_map: dict[int, SolveStatus] = {10: SolveStatus.INTERRUPTED_SAT, 20: SolveStatus.UNSAT, 30: SolveStatus.OPTIMUM, 40: SolveStatus.ERROR, 50: SolveStatus.UNKNOWN}

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, 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.incomplete.TTOpenWBOInc

Bases: OneShotSubprocessReplaySolverBase

TT-Open-WBO-Inc fake-incremental wrapper with one-shot subprocess isolation.

pass_assumptions_to_worker: bool = False

nonunit_soft_policy: str = 'store'

compat_exit_code_status_map: dict[int, SolveStatus] = {10: SolveStatus.OPTIMUM, 20: SolveStatus.UNSAT, 30: SolveStatus.OPTIMUM, 40: SolveStatus.ERROR, 50: SolveStatus.UNKNOWN}

property worker_solver_class_path: str

Import path to worker-side solver class.

property default_signature: str

Default wrapper signature label.

property timeout_error_prefix: str

Name used in timeout error message.

classmethod is_available()

Return type:

bool

__init__(formula=None, *args, default_time_limit=None, time_limit_grace=1.0, timeout_s=None, timeout_grace_s=None, **kwargs)

Parameters:

• formula (WCNF | None)

• default_time_limit (float | None)

• time_limit_grace (float)

• timeout_s (float | None)

• timeout_grace_s (float | 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

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.incomplete.SPBMaxSATCFPS

Bases: OneShotSubprocessReplaySolverBase

SPB-MaxSAT-c-FPS fake-incremental wrapper with one-shot subprocess isolation.

pass_assumptions_to_worker: bool = True

nonunit_soft_policy: str = 'relax'

property worker_solver_class_path: str

Import path to worker-side solver class.

property default_signature: str

Default wrapper signature label.

property timeout_error_prefix: str

Name used in timeout error message.

classmethod is_available()

Return type:

bool

__init__(formula=None, *args, default_time_limit=None, time_limit_grace=1.0, timeout_s=None, timeout_grace_s=None, **kwargs)

Parameters:

• formula (WCNF | None)

• default_time_limit (float | None)

• time_limit_grace (float)

• timeout_s (float | None)

• timeout_grace_s (float | 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

compat_exit_code_status_map: dict[int, SolveStatus] = {10: SolveStatus.INTERRUPTED_SAT, 20: SolveStatus.UNSAT, 30: SolveStatus.OPTIMUM, 40: SolveStatus.ERROR, 50: SolveStatus.UNKNOWN}

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, 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.incomplete.NuWLSCIBR

Bases: OneShotSubprocessReplaySolverBase

NuWLS-c-IBR fake-incremental wrapper with one-shot subprocess isolation.

pass_assumptions_to_worker: bool = True

nonunit_soft_policy: str = 'relax'

property worker_solver_class_path: str

Import path to worker-side solver class.

property default_signature: str

Default wrapper signature label.

property timeout_error_prefix: str

Name used in timeout error message.

classmethod is_available()

Return type:

bool

__init__(formula=None, *args, default_time_limit=None, time_limit_grace=1.0, timeout_s=None, timeout_grace_s=None, **kwargs)

Parameters:

• formula (WCNF | None)

• default_time_limit (float | None)

• time_limit_grace (float)

• timeout_s (float | None)

• timeout_grace_s (float | 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

compat_exit_code_status_map: dict[int, SolveStatus] = {10: SolveStatus.INTERRUPTED_SAT, 20: SolveStatus.UNSAT, 30: SolveStatus.OPTIMUM, 40: SolveStatus.ERROR, 50: SolveStatus.UNKNOWN}

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, 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.incomplete.Loandra

Bases: OneShotSubprocessReplaySolverBase

Loandra fake-incremental wrapper with one-shot subprocess isolation.

pass_assumptions_to_worker: bool = False

property worker_solver_class_path: str

Import path to worker-side solver class.

property default_signature: str

Default wrapper signature label.

property timeout_error_prefix: str

Name used in timeout error message.

classmethod is_available()

Return type:

bool

__init__(formula=None, *args, default_time_limit=None, time_limit_grace=1.0, timeout_s=None, timeout_grace_s=None, **kwargs)

Parameters:

• formula (WCNF | None)

• default_time_limit (float | None)

• time_limit_grace (float)

• timeout_s (float | None)

• timeout_grace_s (float | 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

compat_exit_code_status_map: dict[int, SolveStatus] = {10: SolveStatus.INTERRUPTED_SAT, 20: SolveStatus.UNSAT, 30: SolveStatus.OPTIMUM, 40: SolveStatus.ERROR, 50: SolveStatus.UNKNOWN}

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

Notes

• Assumptions are emulated by adding temporary hard unit clauses to the one-shot solve snapshot.

• Hermax recomputes costs from the returned model in several wrappers to protect against solver bugs.

References

• Mingming Jin, Kun He, Jiongzhi Zheng, Jinghui Xue, Zhuo Chen. Combining BandMaxSAT and FPS with SPB-MaxSAT-c. MaxSAT Evaluation 2024: Solver and Benchmark Descriptions, 2024.

• Ruben Martins, Vasco Manquinho, Ines Lynce. Open-WBO: A Modular MaxSAT Solver. SAT 2014.

• Saurabh Joshi, Prateek Kumar, Sukrut Rao, Ruben Martins. Open-WBO-Inc: Approximation Strategies for Incomplete Weighted MaxSAT. Journal on Satisfiability, Boolean Modelling and Computation 11(1), 2019.

• Alexander Nadel. TT-Open-WBO-Inc: an efficient anytime MaxSAT solver. Journal on Satisfiability, Boolean Modelling and Computation 15(1), 2024.

• Alexander Nadel. Polarity and Variable Selection Heuristics for SAT-Based Anytime MaxSAT: System Description. Journal on Satisfiability, Boolean Modelling and Computation 12(1), 2020.

• Jeremias Berg, Emir Demirovic, Peter J. Stuckey. Core-Boosted Linear Search for Incomplete MaxSAT. CPAIOR 2019.

• Menghua Jiang. NuWLS-c-IBR. MaxSAT Evaluation solver description, 2023.