Non-Incremental Solvers

List of Classes

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

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.