Bindings Reference#

Documents the pybind11-level APIs exposed by Hermax C/C++ extensions. Method names and signatures below are the exact Python names exported by the PYBIND11_MODULE definitions.

pybind11#

A big thanks to the pybind11 project: pybind/pybind11

pybind11 has made building and maintaining Hermax Python bindings substantially simpler.

Conventions#

  • Literals are signed integers (DIMACS style), and literal 0 is invalid.

  • Clause arguments are list[int].

  • weight=None means hard clause; weight as integer means soft clause.

  • IPAMIR-like return codes used by several bindings:

    • 30: optimum found

    • 20: unsatisfiable

    • 10: interrupted with feasible solution

    • 0: interrupted without feasible solution

UWrMaxSAT (IPAMIR)#

class urmaxsat_py.UWrMaxSAT#
newVar() → int#

Allocate and return a fresh variable index (1-based).

addClause(clause: list[int], weight: int | None = None) → None#

Add a clause. Hard if weight is None. Soft otherwise. Non-unit soft clauses are internally relaxed with an auxiliary variable.

assume(assumptions: list[int]) → None#

Add solve-time assumptions for the next solve() call.

solve() → int#

Run the solver and return an IPAMIR status code.

getCost() → int#

Return the current objective value.

getValue(lit: int) → bool | None#

Return True if literal is satisfied, False if falsified, else None when value is unavailable.

set_terminate(callback: Callable[[], int] | None) → None#

Install or clear termination callback.

signature() → str#

Return backend signature string.

Warning

Hermax package builds compile with SCIP integration disabled.

UWrMaxSAT#

class urmaxsat_comp_py.UWrMaxSAT#

Same API as urmaxsat_py.UWrMaxSAT: newVar, addClause, assume, solve, getCost, getValue, set_terminate, signature.

Warning

Hermax package builds compile with SCIP integration disabled.

CASHWMaxSAT#

class cashwmaxsat.CASHWMaxSAT#
newVar() → int#

Allocate and return a fresh variable index.

addClause(clause: list[int], weight: int | None = None) → None#

Add hard/soft clause. Non-unit soft clauses are relaxed via an aux var.

setNoScip() → None#

Disable SCIP integration in CASHWMaxSAT backend.

Note

Hermax compiles with SCIP disabled.

assume(assumptions: list[int]) → None#

Add assumptions for next solve.

solve() → int#

Solve and return IPAMIR status code.

getCost() → int#

Return current objective value.

getValue(lit: int) → bool | None#

Return literal value in current model, or None if unavailable.

set_terminate(callback: Callable[[], int] | None) → None#

Install or clear termination callback.

signature() → str#

Return backend signature string.

EvalMaxSAT#

class evalmaxsat_latest.EvalMaxSAT#
newVar(decisionVar: bool = True) → int#

Allocate a fresh variable (optionally as decision variable).

addClause(clause: list[int], weight: int | None = None) → int#

Add hard or soft clause. Returns backend result code/aux identifier from EvalMaxSAT core.

solve() → bool#

Solve instance; True on satisfiable/optimum state.

getCost() → int#

Return objective value.

getValue(lit: int) → bool#

Return truth value of literal in current model.

getModel() → list[int]#

Return full signed assignment vector [±1, ±2, ...].

setNInputVars(n: int) → None#

Set number of input variables in backend.

Warning

EvalMaxSAT bindings are currently unstable on macOS (arm64 and x86_64) and may crash on some weighted-core test patterns.

EvalMaxSAT (IPAMIR)#

class evalmaxsat_incr.EvalMaxSATIncr#
addClause(clause: list[int], weight: int | None = None) → None#

Add hard clause or unit soft clause. Non-unit soft clauses raise RuntimeError and must be encoded via relaxation in Python.

addSoftLit(lit: int, weight: int) → None#

Add a native soft literal term.

assume(assumptions: list[int]) → None#

Add assumptions for next solve.

solve() → int#

Solve and return IPAMIR status code.

getCost() → int#

Return objective value of the last successful solve.

getValue(lit: int) → bool | None#

Return literal truth value in current model, else None.

signature() → str#

Return backend signature string.

Open-WBO-Inc (Incomplete)#

class openwbo_inc.OpenWBOInc#
newVar() → int#

Allocate and return a fresh variable index.

addClause(clause: list[int], weight: int | None = None) → None#

Add hard or soft clause depending on weight.

solve() → bool#

Solve and return whether a satisfying/optimal model was produced.

getCost() → int#

Return objective value for latest solve call.

getValue(var: int) → bool#

Return assignment for 1-based variable var.

TT Open-WBO-Inc (Incomplete)#

class tt_openwbo_inc.TTOpenWBOInc#
newVar() → int#

Allocate and return a fresh variable index.

addClause(clause: list[int], weight: int | None = None) → None#

Add hard or soft clause depending on weight.

solve() → bool#

Solve and return whether a satisfying/optimal model was produced.

getCost() → int#

Return objective value for latest solve call.

getValue(var: int) → bool#

Return assignment for 1-based variable var.

Open-WBO Algorithms#

class openwbo.OLL#
class openwbo.PartMSU3#
class openwbo.Auto#

Shared API:

newVar() → int#

Allocate fresh external variable id.

addClause(clause: list[int], weight: int | None = None) → None#

Register clause in internal history. Validates literals and weights.

solve(assumptions: list[int] | None = None) → bool#

Rebuild formula and solve with selected algorithm.

getCost() → int#

Return current cost after solve.

getValue(var: int) → bool#

Return variable assignment for 1-based var in latest model.

Loandra#

class loandra.Loandra#
newVar() → int#

Allocate and return a fresh variable index.

addClause(clause: list[int], weight: int | None = None) → None#

Add hard or soft clause.

solve() → bool#

Solve the current instance.

getCost() → int#

Return objective value.

getValue(var: int) → bool#

Return assignment for 1-based variable var.

getModel() → list[int]#

Return full signed assignment vector [±1, ±2, ...].

NuWLS-c-IBR#

class nuwls_c_ibr.NuWLSCIBR#
newVar() → int#

Allocate and return a fresh variable index.

setNInputVars(n: int) → None#

Set number of input variables used by the backend.

addClause(clause: list[int], weight: int | None = None) → None#

Add hard or soft clause.

solve(assumptions: list[int] | None = None) → bool#

Solve the current instance.

getCost() → int#

Return objective value.

getValue(var: int) → bool#

Return assignment for 1-based variable var.

getModel() → list[int]#

Return full signed assignment vector [±1, ±2, ...].

SPB-MaxSAT-c-FPS#

class spb_maxsat_c_fps.SPBMaxSATCFPS#
newVar() → int#

Allocate and return a fresh variable index.

setNInputVars(n: int) → None#

Set number of input variables used by the backend.

addClause(clause: list[int], weight: int | None = None) → None#

Add hard or soft clause.

solve(assumptions: list[int] | None = None) → bool#

Solve the current instance.

getCost() → int#

Return objective value.

getValue(var: int) → bool#

Return assignment for 1-based variable var.

getModel() → list[int]#

Return full signed assignment vector [±1, ±2, ...].

WMaxCDCL#

class wmaxcdcl.WMaxCDCL#
newVar(decisionVar: bool = True) → int#

Allocate and return a fresh variable index.

addClause(clause: list[int], weight: int | None = None) → None#

Add hard or soft clause.

setNInputVars(n: int) → None#

Set number of input variables used by the backend.

prepare() → None#

Prepare internal state before solving.

solve(assumptions: list[int] | None = None) → bool#

Solve the current instance.

getCost() → int#

Return objective value.

getValue(var: int) → bool#

Return assignment for 1-based variable var.

getModel() → list[int]#

Return full signed assignment vector [±1, ±2, ...].

References#

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

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

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

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

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

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

  • 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.

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

  • 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.

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

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

On this page