Aperture: an Anytime, Complete and Incremental MaxSAT Solver

Background: MaxSAT

Background: Anytime MaxSAT

Background: Anytime MaxSAT Today

• State-of-the-art anytime MaxSAT solvers are variations of�tt-open-wbo-inc¹ based on Open-WBO-Inc², which in turn, is based on Open-WBO³.
• The gaps:

​

​

• *Unweighted and Weighted MaxSAT flows are separate, with unnecessary duplication.
• Legacy and dead code parts.

[1] https://github.com/alexander-nadel-academic/tt-open-wbo-inc

[2] https://github.com/sbjoshi/Open-WBO-Inc

[3] https://github.com/sat-group/open-wbo

Aperture

• We introduce Aperture – a brand new anytime MaxSAT solver.
• Developed from scratch in C++ 20.
• Features:

​

​

​

• MaxSAT Evaluation (MSE) 2026:
• Anytime Weighted 🥇60s 🥇300s 🥇1707s
• Anytime Unweighted 🥉60s 🥇300s 🥈1707s

https://github.com/YamSln/Aperture

MaxSAT Solving Flow

• Aperture’s MaxSAT solving flow is unified for weighted and unweighted.

Initial SAT

Local Search

Idle

MrsBeaver

Linear Search SAT-UNSAT

Polosat

SAT

MaxSAT Solving Flow

• Aperture’s MaxSAT solving flow is unified for weighted and unweighted.

Initial SAT

Local Search

Idle

MrsBeaver

Linear Search SAT-UNSAT

Polosat

SAT

Can be invoked incrementally

MaxSAT Solving Flow

• Aperture’s MaxSAT solving flow is unified for weighted and unweighted.

Initial SAT

Local Search

Idle

MrsBeaver

Linear Search SAT-UNSAT

Polosat

SAT

An initial SAT assignment is required

A separate SAT solver might be used.

Even non-incremental, e.g., AE-Kissat-MAB¹.

[1] H. Ding, M. Luo, C. Li, S. Li, R. Chen, C. Xiong, and X. Wu, “AE-Kissat-MAB: Automated evolution of kissat with multi-armed bandits,” in Proceedings of SAT Competition 2025

MaxSAT Solving Flow

• Aperture’s MaxSAT solving flow is unified for weighted and unweighted.

Initial SAT

Local Search

Idle

MrsBeaver

Linear Search SAT-UNSAT

Polosat

SAT

Anytime optimization�Based on incremental SAT solving

Can be interrupted anytime

MaxSAT Solving Flow

• Aperture’s MaxSAT solving flow is unified for weighted and unweighted.

Initial SAT

Local Search

Idle

MrsBeaver

Linear Search SAT-UNSAT

Polosat

SAT

Classic Local Search

Incomplete Part

e.g., SPB-MaxSAT-c-Band¹

[1] M. Jin, K. He, J. Zheng, J. Xue, and Z. Chen, “Combining bandmaxsat and fps with spb-maxsat-c,” in MaxSAT Evaluation 2024

MaxSAT Solving Flow – SAT Based Approx.

• In bit-vector optimization, we treat the bit vector is if it were an unsigned integer, i.e., a weighted is strictly greater than all its preds’.

​

​

​

• Aperture’s utilizes the MrsBeaver^1,2 Algorithm.
• MrsBeaver uses OBV-BS¹, a bit-vector optimization algorithm to approximate MaxSAT.
• It approximates unordered MaxSAT with ordered OBV.

[1] A. Nadel, “Solving maxsat with bit-vector optimization,” SAT 2018

[2] -----------, “Anytime weighted maxsat with improved polarity selection and bit-vector optimization,” FMCAD 2019

1

0

1

1

1

1

0

1

0

. . .

Solve With Negated Assumption

MaxSAT Solving Flow – SAT Based Approx.

[1] A. Nadel, “On optimizing a generic function in sat,” FMCAD 2020

MaxSAT Solving Flow

• Aperture’s MaxSAT solving flow is unified for weighted and unweighted.

Initial SAT

Local Search

Idle

MrsBeaver

Linear Search SAT-UNSAT

Polosat

SAT

Incomplete Part

SAT-based Local Search

MrsBeaver^1,2

• Approximates MaxSAT with bit-vector optimization – OBV-BS¹.
• Calls Polosat³ as a SAT oracle.

[1] A. Nadel, “Solving maxsat with bit-vector optimization,” SAT 2018

[2] -----------, “Anytime weighted maxsat with improved polarity selection and bit-vector optimization,” FMCAD 2019

[3] A. Nadel, “On optimizing a generic function in sat,” FMCAD 2020

MaxSAT Solving Flow

• Aperture’s MaxSAT solving flow is unified for weighted and unweighted.

Initial SAT

Local Search

Idle

MrsBeaver

Linear Search SAT-UNSAT

Polosat

SAT

LSU¹

Complete Part

[1] D. L. Berre and A. Parrain, “The sat4j library, release 2.2,” JSAT, vol. 7, no. 2-3, pp. 59–6, 2010.

Experimental Results: MSE’22-24

• Solvers:
• 2 configurations of Aperture.
• tt-open-wbo-inc.
• MSE’24 winners.
• Results:
• Tops 8/12 MSE’22-24 tracks.
• Tops 4/4 MSE’24 tracks.
• MSE’26^1,2:
• Weighted 🥇60s 🥇300s 🥇1707s
• Unweighted 🥉60s 🥇300s 🥈1707s

​

​

​

[1] https://maxsat-evaluations.github.io/2026/anytime-unweighted-ranking.html

[2] https://maxsat-evaluations.github.io/2026/anytime-weighted-ranking.html

Experimental Results: MSE’22 Incremental

• Solvers:
• Aperture.
• All solvers participated in MSE’22.
• Results:
• Tops 2/5 benchmark families.
• MSE’26:
• Won 1/5 benchmark families.

Beyond Anytime MaxSAT

• Polosat optimizes a black-box PB function.
• The user can provide a custom generic function.

SolverStatus SolveBlackBox(Lits<TLit> assumps, Lits<TLit> observables, std::function<TWeight(std::function<TLitValue(TLit)>, void*)> PbFunc,…)

def solve_black_box(self, assumptions: TLiterals, observables: TLiterals, pb_func: Callable[[TLit], int],…) -> bool

​

• OBV-BS solves the Optimization Modulo Bit-vector (OBV) problem.

SolverStatus SolveOBV(Lits<TLit> assumps, Lits<TLit> targets,…) -> bool

def solve_obv(self, assumptions: TLiterals, targets: TLiterals) -> bool

​

MaxSAT

SAT

BlackBox

OBV

Thank You!