TT-Open-WBO-Inc: The SAT Engine of Modern Anytime MaxSAT

Alexander Nadel

Technion & NVIDIA, Israel

Dagstuhl Seminar on 'Interactions in Constraint Optimization' (25371)

Schloss Dagstuhl, Germany

September 9, 2025

1

MaxSAT: Definition

Extension of SAT to Linear Optimization

2

MaxSAT: Definition

Extension of SAT to Linear Optimization

3

MaxSAT

• MaxSAT is widely applied
• Domains: AI, data mining, scheduling, verification, …
• Tasks: planning, optimization, structure learning, debugging, physical design in CAD, …
• Community:
• >2,000 peer-reviewed papers and major technical reports
• Yearly MaxSAT Evaluations (MSEs) since 2006 (skipped in 2025☹)
• The MaxSAT literature, algorithms, and evaluations are typically category-specific
• Categories:
• Classification by the input: Weighted vs. Unweighted
• Unweighted ≅ all weights are 1
• Classification by the algorithm type: Exact vs. Anytime^1,2
• Exact (formerly in MSEs: complete)
• Guaranteed to return an optimal solution
• No intermediate solutions required
• Anytime (formerly in MSEs: incomplete)
• Not guaranteed to return an optimal solution (but often do)
• Continuously outputs improving solutions
• Crucial for industrial use and hard real-world problems!
• Evaluated at MaxSAT Evaluations since 2011

Usage and Categories

1. Dean, T. L., & Boddy, M. S., "An analysis of time-dependent planning," AAAI 1988.
2. Zilberstein, S., "Using anytime algorithms in intelligent systems," AI Magazine 17(3), 1996.

4

TT-Open-WBO-Inc: The SAT Engine of Modern Anytime MaxSAT

Anytime/Incomplete MSE Winners (2019-2024)

Highlighted: �TT-Open-WBO-Inc inside

MSE 2024: Best Solvers in Anytime Categories

5

TT-Open-WBO-Inc Genealogy

Open-WBO-LSU¹

Open-WBO-Inc-BMO²

Weighted MaxSAT by BMO approximation²

TT-Open-WBO-Inc-2019³

Anytime-MaxSAT-dedicated SAT heuristics⁴

TT-Open-WBO-Inc-2020⁶

• SatLike local search as preprocessing⁵
• Unweighted MaxSAT by OBV approximation (Mrs. Beaver)^4,7
• SAT-based local search (Polosat)⁸

1. Martins, R., Manquinho, V., & Lynce, I., "Open-WBO: A Modular MaxSAT Solver," SAT 2014.
2. Joshi, S., Kumar, P., Rao, S., & Martins, R., "Open-wbo-inc: Approximation strategies for incomplete weighted maxsat," JSAT 2019.
3. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
4. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.
5. Cai, S., & Lei, Z., "Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability," AI 2020.
6. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.
7. Nadel, A., "Solving MaxSAT with Bit-Vector Optimization," SAT 2018.
8. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.
9. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.
10. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.
11. Jin, M., He, K., Zheng, J., Xue, J., & Chen, Z., "Combining BandMaxSAT and FPS with SPB-MaxSAT-c," MSE 2024.

​

TT-Open-WBO-Inc

MSE’21-24

SAT&LS solvers integration & Polosat tuning

Efficient SAT encodings + Linear SAT-UNSAT (LSU) algorithm

SatLike-c⁵

NuWLS-c⁹

NuWLS-c-2023¹⁰

Novelty in local search

SPB-MaxSAT-c*¹¹

6

Linear Search SAT-UNSAT (LSU)¹

7

9/8/2025

1. F 🡨 H // Initializing CNF F with the hard clauses
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F // using a cardinality or a PB constraint
4. Else // UNSAT
• Return the last model M // M is guaranteed to be an optimal model

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

7

Cardinality and Pseudo-Boolean (PB) Constraints

• How to block the models with an upper bound on the weight in LSU?
• Unweighted MaxSAT:
• Cardinality constraint: x₁ + . . . + x_n ≤ b
• Example: x₁ + x₂ + x₃ + x₄ + x₅ ≤ 3
• Weighted MaxSAT:
• PB constraint: l₁*x₁ + . . . + l_n* x_n ≤ b
• Example: 2x₁ + 4x₂ + x₃ + 5x₄ + 7x₅ ≤ 10
• In MaxSAT solving, these constraints are encoded into clauses
• TT-Open-WBO-Inc’s encodings:
• Cardinality Encoding: Totalizer^1,2
• Pseudo-Boolean Encoding: Generalized Totalizer (GTU)³ or Adder⁴ (if |clauses| > 3M)
• Encodings property: the upper bound can be easily & incrementally tightened
• Essential for efficient LSU implementation

​

​

​

​

1. Bailleux, O., & Boufkhad, Y., "Efficient CNF encoding of Boolean cardinality constraints," CP 2003.
2. Büttner, M., & Rintanen, J., "Satisfiability planning with constraints on the number of actions," ICAPS 2005.
3. Joshi, S., Martins, R., & Manquinho, V. M., "Generalized totalizer encoding for pseudo-Boolean constraints," CP 2015.
4. Eén, N., & Sörensson, N., "Translating Pseudo-Boolean Constraints into SAT," JSAT, 2006.

​

8

LSU

Properties and Usage

• Pros ☺
• Inherently anytime
• All the solver invocations, but the last one:
• Return SAT
• Improve the previous best model
• Complete
• Cons ☹
• Cardinality and PB constraints are too heavy
• Convergence might be too slow
• The first model might be too far away
• Finding the next best model might be too slow
• TT-Open-WBO-Inc falls back to LSU when & if:
• Approximations exhausted, and/or
• The cardinality/PB encoding becomes manageable after tightening the upper bound

9

TT-Open-WBO-Inc Genealogy

Open-WBO-LSU¹

Open-WBO-Inc-BMO²

Weighted MaxSAT by BMO approximation²

TT-Open-WBO-Inc-2019³

Anytime-MaxSAT-dedicated SAT heuristics⁴

TT-Open-WBO-Inc-2020⁶

• SatLike local search as preprocessing⁵
• Unweighted MaxSAT by OBV approximation (Mrs. Beaver)^4,7
• SAT-based local search (Polosat)⁸

1. Martins, R., Manquinho, V., & Lynce, I., "Open-WBO: A Modular MaxSAT Solver," SAT 2014.
2. Joshi, S., Kumar, P., Rao, S., & Martins, R., "Open-wbo-inc: Approximation strategies for incomplete weighted maxsat," JSAT 2019.
3. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
4. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.
5. Cai, S., & Lei, Z., "Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability," AI 2020.
6. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.
7. Nadel, A., "Solving MaxSAT with Bit-Vector Optimization," SAT 2018.
8. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.
9. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.
10. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.
11. Jin, M., He, K., Zheng, J., Xue, J., & Chen, Z., "Combining BandMaxSAT and FPS with SPB-MaxSAT-c," MSE 2024.

​

TT-Open-WBO-Inc

MSE’21-24

SAT&LS solvers integration & Polosat Tuning

Efficient SAT encodings + Linear SAT-UNSAT (LSU) algorithm

SatLike-c⁵

NuWLS-c⁹

NuWLS-c-2023¹⁰

Novelty in local search

SPB-MaxSAT-c*¹¹

10

Approximating Weighted MaxSAT by BMO¹

BMO: Boolean Multilevel Optimization²

• The weighted MaxSAT algorithm:
• Cluster target bits by weight
• W = {w₅ = 5, w₄ = 3, w₃ = 5, w₂ = 2, w₁ = 5, w₀ = 3}
• T clustering:
• {t₅, t₃, t₁}
• {t₄, t₀}
• {t₂}
• Incrementally apply unweighted LSU cluster by cluster (highest weight first)
• For every cluster, find a solution with the fewest target bits on and tighten its cardinality constraint accordingly
• Incomplete, might miss solutions. Assume 2 solutions in our example:
• S₁≡{t₅, t₄, t₀} of weight 11
• S₂ ≡{t₅, t₃} of weight 10
• The algorithm will return S₁
• Fall back to weighted LSU
• Undo all the cardinality constraints before
• Bound the PB constraint from above with the best solution’s weight for efficiency
• Properties -- lighter and faster than Weighted LSU:
• Lighter cardinality constraints replace PB constraints for the approximation stage
• Weighted LSU (if reached within timeout) starts from a tightened bound
• Usage in TT-Open-WBO-Inc: applied for Weighted MaxSAT

​

​

​

1. Joshi, S., Kumar, P., Rao, S., & Martins, R., "Open-wbo-inc: Approximation strategies for incomplete weighted maxsat“, JSAT 2019.
2. Argelich, J., Lynce, I., & Marques Silva, J. P., "On solving Boolean multilevel optimization problems," IJCAI 2009.

11

TT-Open-WBO-Inc Genealogy

Open-WBO-LSU¹

Open-WBO-Inc-BMO²

Weighted MaxSAT by BMO approximation²

TT-Open-WBO-Inc-2019³

Anytime-MaxSAT-dedicated SAT heuristics⁴

TT-Open-WBO-Inc-2020⁶

• SatLike local search as preprocessing⁵
• Unweighted MaxSAT by OBV approximation (Mrs. Beaver)^4,7
• SAT-based local search (Polosat)⁸

1. Martins, R., Manquinho, V., & Lynce, I., "Open-WBO: A Modular MaxSAT Solver," SAT 2014.
2. Joshi, S., Kumar, P., Rao, S., & Martins, R., "Open-wbo-inc: Approximation strategies for incomplete weighted maxsat," JSAT 2019.
3. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
4. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.
5. Cai, S., & Lei, Z., "Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability," AI 2020.
6. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.
7. Nadel, A., "Solving MaxSAT with Bit-Vector Optimization," SAT 2018.
8. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.
9. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.
10. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.
11. Jin, M., He, K., Zheng, J., Xue, J., & Chen, Z., "Combining BandMaxSAT and FPS with SPB-MaxSAT-c," MSE 2024.

​

TT-Open-WBO-Inc

MSE’21-24

SAT&LS solvers integration & Polosat Tuning

Efficient SAT encodings + Linear SAT-UNSAT (LSU) algorithm

SatLike-c⁵

NuWLS-c⁹

NuWLS-c-2023¹⁰

Novelty in local search

SPB-MaxSAT-c*¹¹

12

SAT Polarity Selection for Anytime MaxSAT

• TT-Open-WBO-Inc makes many incremental SAT queries in its anytime MaxSAT flows
• The goal: steer the SAT solver’s polarity selection to improve anytime MaxSAT efficiency
• The technique: make every SAT query to always look for the next solution near an assignment M¹
• By biasing the SAT polarity heuristic to select M(v) every time a participating variable v is chosen by the variable decision heuristic
• Conservative: M is the best solution so far (WPM3², LinSBPS³); starts from the 2^nd SAT query
• Locality: it’s easier to find the next best solution in the neighborhood of the previous best one
• Optimistic: M is the ideal assignment -- targets are fixed to 0 (Sat4J⁴)
• The first model and any subsequent model is closer to the ideal
• Target-Optimal-Rest-Conservative -- TORC (TT-Open-WBO-Inc^5,6):
• Takes the best from the conservative and optimistic approaches
• A non-target variable: TORC sets its polarity to its value in the best model so far
• A target variable: TORC sets its polarity to 0
• Results^5,6 [Nadel 2019] [Nadel 2020b]
• TORC > conservative > optimistic > default SAT polarity selection
• For weighted MaxSAT, TORC works well with Target-Score-Bump (TSB) variable boost heuristic^1,2

1. Agbaria, S., Carmi, D., Cohen, O., Korchemny, D., Lifshits, M., & Nadel, A., "SAT-Based Semiformal Verification of Hardware," FMCAD 2010.
2. Ansótegui, C., Gabàs, J., & Levy, J., "Exploiting subproblem optimization in SAT-based MaxSAT algorithms," J. Heuristics, 2016.
3. Berg, J., Demirović, E., & Stuckey, P., "Core-Boosted Linear Search for Incomplete MaxSAT," CPAIOR 2019.
4. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.
5. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
6. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.

​

13

SAT Variable Decision Heuristic Adjustment for Anytime MaxSAT

Target-Score-Bump (TSB) Heuristic^1,2

• Observation: the impact of the TORC/optimistic polarity selection depends on the variable order
• Target bit selected by the variable decision heuristic 🡪 0 polarity applied
• Target bit propagated by BCP 🡪 unknown polarity forced by the SAT solver
• Core idea: adjust variable selection order by boosting scores of target variables
• Boosting factor is configurable
• Trade-off:
• Boost = ∞: always start with target bits, negated (except for propagated target bits)
• Equivalent to setting the negated targets as assumptions
• Botches SAT variable decision heuristic -- extremely slow in practice
• Boost = 0: no influence
• Implementation in TT-Open-WBO-Inc:
• Balanced scheme:
• Apply moderate boost to favor target variables at the beginning
• Include a weight bias
• Let the SAT solver adjust the scores as usual based on conflict-analysis
• See ¹ for TSB’s magic numbers & positive experimental results for weighted MaxSAT
• Pays off only for weighted MaxSAT³

​

​

1. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
2. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.
3. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.

​

14

TT-Open-WBO-Inc Genealogy

Open-WBO-LSU¹

Open-WBO-Inc-BMO²

Weighted MaxSAT by BMO approximation²

TT-Open-WBO-Inc-2019³

Anytime-MaxSAT-dedicated SAT heuristics⁴

TT-Open-WBO-Inc-2020⁶

• SatLike local search as preprocessing⁵
• Unweighted MaxSAT by OBV approximation (Mrs. Beaver)^4,7
• SAT-based local search (Polosat)⁸

1. Martins, R., Manquinho, V., & Lynce, I., "Open-WBO: A Modular MaxSAT Solver," SAT 2014.
2. Joshi, S., Kumar, P., Rao, S., & Martins, R., "Open-wbo-inc: Approximation strategies for incomplete weighted maxsat," JSAT 2019.
3. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
4. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.
5. Cai, S., & Lei, Z., "Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability," AI 2020.
6. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.
7. Nadel, A., "Solving MaxSAT with Bit-Vector Optimization," SAT 2018.
8. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.
9. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.
10. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.
11. Jin, M., He, K., Zheng, J., Xue, J., & Chen, Z., "Combining BandMaxSAT and FPS with SPB-MaxSAT-c," MSE 2024.

​

TT-Open-WBO-Inc

MSE’21-24

SAT&LS solvers integration & Polosat Tuning

Efficient SAT encodings + Linear SAT-UNSAT (LSU) algorithm

SatLike-c⁵

NuWLS-c⁹

NuWLS-c-2023¹⁰

Novelty in local search

SPB-MaxSAT-c*¹¹

15

TT-Open-WBO-Inc-2020: the Algorithmics

M := SAT(H)

​

​

M := LocalSearch(M)

Incremental SAT-based Flow

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

TORC polarity selection

Weighted: TSB variable boost

Fallback to LSU?

TORC polarity selection

Weighted: TSB variable boost

​

​

​

​

​

​

​

​

​

​

​

​

​

Polosat became too slow?

Approximation: BMO -- weighted; Mrs. Beaver (OBV) -- unweighted

SAT

Polosat: SAT-based Local Search

SAT

Yes

No

16

Optimization modulo Bitvectors (OBV)

by Reduction to MaxSAT

OBV vs. MaxSAT solving: The order makes OBV easier than MaxSAT

17

OBV-BS Algorithm for OBV Solving^1,2

Iteratively try fixing target bits to 0, in order from MSB to LSB

OBV-BS

• M := SAT(H)
• i := n-1
• FixBlockTo0(i, M)
• While (i ≥ 0)
• M := SAT(H, ¬t_i)
• If SAT
• FixBlockTo0(i, M)
• Else (UNSAT)
• H := H ∧ t_i; i := i - 1
• Return M

Input: Hard Constraints (Clauses) H

Optimization target: T = [t_n-1 t_n-2 … t₀]

Output: A model M to H which minimizes T’s value

• T is interpreted as an unweighted integer with t_n-1 being the MSB

​

FixBlockTo0(i, M) // i is provided by reference

While (i ≥ 0 and M(t_i) = 0) {H := H ∧ ¬t_i; i := i – 1}

​

1. Knuth, D. E., "The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability," Addison-Wesley, 2015.
2. Nadel, A., & Ryvchin, V., "Bit-Vector Optimization," TACAS 2016.

18

Mrs. Beaver^1,2

Approximate MaxSAT by OBV-BS

• Sub-procedures
• OBV-BS
• UMS-OBV-BS: OBV-BS modified to satisfy fewer target bits on-the-fly
• Whenever there is a model, all the falsified target bits are shifted towards the MSB
• Doesn’t solve OBV anymore
• Mrs. Beaver(M) // M: the best solution so far
• Loop forever or until the cardinality/PB encoding is small enough for LSU to digest:
• Run UMS-OBV-BS(T). Update M, if a better solution is found.
• Reverse T. Run UMS-OBV-BS(T). Update M, if a better solution is found.
• Reverse T. Run OBV-BS(T). Update M, if a better solution is found.
• Reverse T. Run OBV-BS(T). Update M, if a better solution is found.
• Randomly shuffle T
• LSU(M)
• Mrs. Beaver’s properties:
• Efficient incomplete approximation -- never creates cardinality/PB constraints unless the size is manageable enough to fall back to LSU
• Attempts to diversify the solution space by switching between algorithms & shuffling the target
• Usage in TT-Open-WBO-Inc: implemented and applied for unweighted MaxSAT only
• Can be easily adjusted for weighted MaxSAT²

1. Nadel, A., "Solving MaxSAT with Bit-Vector Optimization," SAT 2018.
2. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.

19

TT-Open-WBO-Inc-2020: the Algorithmics

M := SAT(H)

​

​

M := LocalSearch(M)

Incremental SAT-based Flow

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

TORC polarity selection

Weighted: TSB variable boost

Fallback to LSU?

TORC polarity selection

Weighted: TSB variable boost

​

​

​

​

​

​

​

​

​

​

​

​

​

Polosat became too slow?

Approximation: BMO -- weighted; Mrs. Beaver (OBV) -- unweighted

SAT

Polosat: SAT-based Local Search

SAT

Yes

No

20

Polosat¹: Optimizing a Black-Box Function in SAT

SAT-based local search (local search with SAT as an oracle)

1. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.

Implementation details, crucial for efficiency:

• Using a conflict threshold (1000) to limit every SAT query
• Applying TORC / conservative polarity heuristic: steers Polosat into performing local search around the best model

21

Polosat¹: Optimizing a Black-Box Function in SAT

Properties & Observations

• Anytime
• Incomplete
• In practice, crucial for TT-Open-WBO-Inc’s efficiency (both weighted & unweighted MaxSAT)²
• Classical local search and SAT-based search (Polosat) are complementary
• Weighted: Polosat-OBV – a variant that is even more efficient²
• Can be successfully applied beyond MaxSAT for optimizing black-box functions without translating them to clauses¹

​

1. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.
2. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.

22

TT-Open-WBO-Inc-2020: the Algorithmics

M := SAT(H)

​

​

M := LocalSearch(M)

Incremental SAT-based Flow

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

TORC polarity selection

Weighted: TSB variable boost

Fallback to LSU?

TORC polarity selection

Weighted: TSB variable boost

​

​

​

​

​

​

​

​

​

​

​

​

​

Polosat became too slow?

Approximation: BMO -- weighted; Mrs. Beaver (OBV) -- unweighted

SAT

Polosat: SAT-based Local Search

SAT

Yes

No

23

TT-Open-WBO-Inc-2020: the Algorithmics

M := SAT(H)

​

​

M := LocalSearch(M)

Incremental SAT-based Flow

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

TORC polarity selection

Weighted: TSB variable boost

Fallback to LSU?

TORC polarity selection

Weighted: TSB variable boost

​

​

​

​

​

​

​

​

​

​

​

​

​

Polosat became too slow?

Approximation: BMO -- weighted; Mrs. Beaver (OBV) -- unweighted

SAT

Polosat: SAT-based Local Search

SAT

Yes

No

24

MaxSAT: Definition in Terms of Clauses

• Input
• Hard clauses H
• Weighted soft clauses S
• Output
• Solution to H, such that:
• The total weight of falsified soft clauses is minimal

SAT with Soft Clauses

25

Local Search in TT-Open-WBO-Inc

Shared Fundamentals

• Always maintain:
• the current best solution α*
• a complete assignment α
• Both α* and α are initialized by the initial SAT query over the hard clauses
• Loop till timeout
• (Re)init weights of every clause (hard and soft)
• LS round: loop for S steps (S initialized to 10⁷)
• If α is a solution better than α* (satisfies more soft clauses, weighted)
• α* := α
• Increase S by 10⁷
• Flip a variable in α with the highest score > 0, if such exists
• make = weight of clauses that become satisfied if x is flipped
• break = weight of clauses that become falsified if x is flipped
• score = make – break
• The local minimum case (all variables have score ≤ 0)
• Update clause weights
• If all the clauses (hard and soft) are satisfied (optimal solution found) 🡪 exit
• If a hard clause is falsified 🡪 c := a random falsified hard clause
• Otherwise 🡪 c := a random falsified soft clause
• Flip in α a variable with the highest score in c
• Return α*

​

Not the original weight of soft clauses!

More precisely: apply BMS -- picks a random var. out of best t with replacement

Lurking here: weights handling that sets the algorithms apart:

1. Init weights
2. Reinit weights (if any)
3. Update weights at local optima

• Weights initialization
• Weights reinitialization (if any)

• Weights initialization
• Weights reinitialization (if any)

• Weights initialization
• Weights reinitialization (if any)

26

TT-Open-WBO-Inc Genealogy

Open-WBO-LSU¹

Open-WBO-Inc-BMO²

Weighted MaxSAT by BMO approximation²

TT-Open-WBO-Inc-2019³

Anytime-MaxSAT-dedicated SAT heuristics⁴

TT-Open-WBO-Inc-2020⁶

• SatLike local search as preprocessing⁵
• Unweighted MaxSAT by OBV approximation (Mrs. Beaver)^4,7
• SAT-based local search (Polosat)⁸

1. Martins, R., Manquinho, V., & Lynce, I., "Open-WBO: A Modular MaxSAT Solver," SAT 2014.
2. Joshi, S., Kumar, P., Rao, S., & Martins, R., "Open-wbo-inc: Approximation strategies for incomplete weighted maxsat," JSAT 2019.
3. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
4. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.
5. Cai, S., & Lei, Z., "Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability," AI 2020.
6. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.
7. Nadel, A., "Solving MaxSAT with Bit-Vector Optimization," SAT 2018.
8. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.
9. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.
10. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.
11. Jin, M., He, K., Zheng, J., Xue, J., & Chen, Z., "Combining BandMaxSAT and FPS with SPB-MaxSAT-c," MSE 2024.

​

TT-Open-WBO-Inc

MSE’21-24

SAT&LS solvers integration & Polosat Tuning

Efficient SAT encodings + Linear SAT-UNSAT (LSU) algorithm

SatLike-c⁵

NuWLS-c⁹

NuWLS-c-2023¹⁰

Novelty in local search

SPB-MaxSAT-c*¹¹

27

SatLike Local Search Algorithm¹

• A performance breakthrough vs. earlier approaches^[2-8] to local search for MaxSAT
• Both as stand-alone and as a preprocessor before SAT-based flow
• The idea:
• Previous works’ weights handling put too much emphasis on hard clauses
• The algorithms get stuck around the initial feasible solution, which might be far away for the optimum
• Solution: prefer the soft clauses over the hard clauses at the beginning!
• Implementation through weights handling:
• Init weights:
• For each hard clause, associate an integer as its weight, initialized to 1
• For each soft clause, use the original weight as its initial weight
• Initially, the soft clauses are more important than the hard ones!
• Reinit weights: none
• Update weights at local optima:
• For each falsified hard clause, increase its weight by h, where h >= 1 (h=1 for unweighted; h=3 for weighted)
• For each falsified soft clause with weight < T, increase its weight by 1 (unweighted: T=1 if vars < 1100 else 400; weighted: T=1 if avrg_origw < 10000 else 500)
• Hard clauses become dominating as the time goes by (because of the threshold on the soft clause weights)!

​

1. Cai, S., & Lei, Z., "Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability," AI 2020.
2. Pierre Hansen, Brigitte Jaumard., “Algorithms for the Maximum Satisfiability Problem,” Computing 44, 279- 303, 1990.
3. Yuejun Jiang, Henry Kautz, Bart Selman. “Solving Problems with Hard and Soft Constraints Using a Stochastic Algorithm for MAX-SAT”, Proc. 1st Intl. Joint Workshop on AI & OR, Timberline, Oregon., Timberline, Oregon USA, 1995.
4. H. Hoos, T Stützle., “Stochastic local search: Foundations and applications,” Elsevier/Morgan Kaufmann, 2005
5. Smyth, B., Hoos, H., & Stützle, T., "An adaptive algorithm for solving MAX-SAT problems," AI 2003.
6. Tompkins, D. A. D., "Dynamic Local Search for SAT: Design, Insights and Analysis," PhD Thesis, University of British Columbia, October 2010.
7. Luo, C., Cai, S., Wu, J., Jie, Y., & Su, K., "An effective algorithm for weighted MAX-SAT," AI 2015.
8. Cai, S., Luo, C., Lin, Z., & Su, K., "Improved local search for weighted maximum satisfiability," AI 2016.

28

TT-Open-WBO-Inc Genealogy

Open-WBO-LSU¹

Open-WBO-Inc-BMO²

Weighted MaxSAT by BMO approximation²

TT-Open-WBO-Inc-2019³

Anytime-MaxSAT-dedicated SAT heuristics⁴

TT-Open-WBO-Inc-2020⁶

• SatLike local search as preprocessing⁵
• Unweighted MaxSAT by OBV approximation (Mrs. Beaver)^4,7
• SAT-based local search (Polosat)⁸

1. Martins, R., Manquinho, V., & Lynce, I., "Open-WBO: A Modular MaxSAT Solver," SAT 2014.
2. Joshi, S., Kumar, P., Rao, S., & Martins, R., "Open-wbo-inc: Approximation strategies for incomplete weighted maxsat," JSAT 2019.
3. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
4. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.
5. Cai, S., & Lei, Z., "Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability," AI 2020.
6. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.
7. Nadel, A., "Solving MaxSAT with Bit-Vector Optimization," SAT 2018.
8. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.
9. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.
10. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.
11. Jin, M., He, K., Zheng, J., Xue, J., & Chen, Z., "Combining BandMaxSAT and FPS with SPB-MaxSAT-c," MSE 2024.

​

TT-Open-WBO-Inc

MSE’21-24

SAT&LS solvers integration & Polosat Tuning

Efficient SAT encodings + Linear SAT-UNSAT (LSU) algorithm

SatLike-c⁵

NuWLS-c⁹

NuWLS-c-2023¹⁰

Novelty in local search

SPB-MaxSAT-c*¹¹

29

NuWLS Local Search Algorithm¹

Improving SatLike

• Observations:
• Small average original weight (including unweighted instances) 🡪 enlarging initial soft clause weights is beneficial
• Large average original weight 🡪 reducing initial soft clause weights is beneficial
• The status of α matters (feasible at the local optima? already found a solution this round? found a better solution this round?)
• Implementation through weights handling:
• Init and reinit weights:
• Hards: 1
• Softs:
• Initially or if a solution is not found in the last round 🡪 1
• Prioritize hard clauses to find a solution
• Otherwise:

​

• Update weights of falsified hard and soft clauses at local optima; main changes w.r.t SatLike:
• Hard clauses:
• Solution found in the current round 🡪 smooth the hard clause weights (applied with a certain probability)
• Soft clauses:
• A better solution found in this round (cost(α) < cost(α∗)) 🡪 the soft clause weights are not updated (to stay around α)
• Solution still not found in current round 🡪 the soft clause weights is not increased.

1. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.

30

TT-Open-WBO-Inc Genealogy

Open-WBO-LSU¹

Open-WBO-Inc-BMO²

Weighted MaxSAT by BMO approximation²

TT-Open-WBO-Inc-2019³

Anytime-MaxSAT-dedicated SAT heuristics⁴

TT-Open-WBO-Inc-2020⁶

• SatLike local search as preprocessing⁵
• Unweighted MaxSAT by OBV approximation (Mrs. Beaver)^4,7
• SAT-based local search (Polosat)⁸

1. Martins, R., Manquinho, V., & Lynce, I., "Open-WBO: A Modular MaxSAT Solver," SAT 2014.
2. Joshi, S., Kumar, P., Rao, S., & Martins, R., "Open-wbo-inc: Approximation strategies for incomplete weighted maxsat," JSAT 2019.
3. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
4. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.
5. Cai, S., & Lei, Z., "Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability," AI 2020.
6. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.
7. Nadel, A., "Solving MaxSAT with Bit-Vector Optimization," SAT 2018.
8. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.
9. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.
10. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.
11. Jin, M., He, K., Zheng, J., Xue, J., & Chen, Z., "Combining BandMaxSAT and FPS with SPB-MaxSAT-c," MSE 2024.

​

TT-Open-WBO-Inc

MSE’21-24

SAT&LS solvers integration & Polosat Tuning

Efficient SAT encodings + Linear SAT-UNSAT (LSU) algorithm

SatLike-c⁵

NuWLS-c⁹

NuWLS-c-2023¹⁰

Novelty in local search

SPB-MaxSAT-c*¹¹

31

NuWLS-2023 Local Search Algorithm¹

Research Questions in ¹

• Init and reinit:
• How to initialize and adjust the weight of each hard clause and each soft clause to distinguish between them during the search?
• In particular, what is the increment to be added to the weight of a soft clause?
• Threshold on the weights:
• Can the weight of a clause be infinitely increased?
• In other words, should there be an upper bound for the weight of a clause?
• If yes, what is the upper bound?
• Should it be uniform for all clauses or specific for each clause?
• Update weights at local optima
• How to select the clauses whose weights should be adjusted?

1. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.

32

NuWLS-2023 Local Search Algorithm¹

The Algorithm

1. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.

• Focus on finding a feasible solution first (both init and reinit)

​

• The weight of each soft clause is increased at a local optimum
• as opposite to falsified only

​

• The hierarchy between soft clauses is always kept
• Given any two soft clauses c₁ and c₂, if w_ori(c₁) ≤ w_ori(c₂), then w(c₁) ≤ w(c₂) for any k.
• The difference of weights between c₁ and c₂ keeps increasing with the number of feasible local optima k
• The more feasible local optima, the more important the soft clauses with large original weight will be

​

• The more feasible local optima, the more important soft clauses become w.r.t hard clauses
• No threshold (upper bound) in contrast to previous approaches!

​

• Infeasible vs. feasible local optimum
• Infeasible local optimum 🡪 hard weights increased
• Feasible local optimum 🡪 soft weights increased

​

• The best solution found so far in terms of Unified-SW’s weights = the best solution found so far in terms of original weights.

​

33

TT-Open-WBO-Inc Genealogy

Open-WBO-LSU¹

Open-WBO-Inc-BMO²

Weighted MaxSAT by BMO approximation²

TT-Open-WBO-Inc-2019³

Anytime-MaxSAT-dedicated SAT heuristics⁴

TT-Open-WBO-Inc-2020⁶

• SatLike local search as preprocessing⁵
• Unweighted MaxSAT by OBV approximation (Mrs. Beaver)^4,7
• SAT-based local search (Polosat)⁸

1. Martins, R., Manquinho, V., & Lynce, I., "Open-WBO: A Modular MaxSAT Solver," SAT 2014.
2. Joshi, S., Kumar, P., Rao, S., & Martins, R., "Open-wbo-inc: Approximation strategies for incomplete weighted maxsat," JSAT 2019.
3. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
4. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.
5. Cai, S., & Lei, Z., "Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability," AI 2020.
6. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.
7. Nadel, A., "Solving MaxSAT with Bit-Vector Optimization," SAT 2018.
8. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.
9. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.
10. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.
11. Jin, M., He, K., Zheng, J., Xue, J., & Chen, Z., "Combining BandMaxSAT and FPS with SPB-MaxSAT-c," MSE 2024.

​

TT-Open-WBO-Inc

MSE’21-24

SAT&LS solvers integration & Polosat Tuning

Efficient SAT encodings + Linear SAT-UNSAT (LSU) algorithm

SatLike-c⁵

NuWLS-c⁹

NuWLS-c-2023¹⁰

Novelty in local search

SPB-MaxSAT-c*¹¹

34

SPB-MaxSAT Local Search Algorithm¹

• Main idea:
• Adapt local search’s score to decrease the value of the following SPB constraint:

SPB(α) := total original-weight of falsified soft clauses in α

• Guides the search to improve MaxSAT’s objective function
• How:
• Weight the hard clauses similarly to previous approaches
• Weight SPB as a whole instead of weighting the soft clauses individually
• Soft clauses are not part of the equation weighting scheme anymore!
• Implementation:
• Score function in the previous algorithms:
• Flip a variable in α with the highest score > 0, if such exists
• make = weight of clauses that become satisfied if x is flipped
• break = weight of clauses that become falsified if x is flipped
• score = make – break

​

1. Zheng, J., Chen, Z., Li, C.-M., & He, K., "Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers," IJCAI 2024.

35

SPB-MaxSAT Local Search Algorithm¹

• Main idea:
• Adapt local search’s score to mind (and increase) the value of the following SPB constraint:

SPB(α) := total original-weight of falsified soft clauses in α

• Guides the search to improve MaxSAT’s objective function
• How:
• Weight the hard clauses similarly to previous approaches
• Weight SPB as a whole instead of weighting the soft clauses individually
• Soft clauses are not part of the equation weighting scheme anymore!
• Implementation:
• Score function in the previous algorithms SPB-MaxSAT:
• Flip a variable x in α with the highest score > 0, if such exists
• make = weight of hard clauses that become satisfied if x is flipped + w_spb ⋅ SPB(α)
• break = weight of hard clauses that become falsified if x is flipped + w_spb ⋅ SPB(α’) // α’ is α after flipping x
• score = make – break
• Init weights:
• Set the weight of each hard clause and the SPB to 1
• Reinit weights: none
• Update weights at local optima:
• For each falsified hard clause, increase its weight by h_inc, where h_inc=1 for unweighted; h_inc=28 for weighted
• If SPB(α) ≥ SPB(α*), w_spb := δ ⋅ (w_spb + 1), where δ =1.00072 for unweighted; δ =1.001 for weighted

​

1. Zheng, J., Chen, Z., Li, C.-M., & He, K., "Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers," IJCAI 2024.

36

SPB-MaxSAT-c-Band and SPB-MaxSAT-c-FPS

Combining SPB² with Band³ and FPS⁴ to MSE’24¹

• Three version of SPB-MaxSAT, submitted to MSE’24:
• (Plain) SPB-MaxSAT-c
• c stands for complete to reflect the fact that a complete solver (TT-Open-WBO-Inc-2020) is invoked after the local search
• SPB-MaxSAT-c-Band
• Combination with ³: soft clauses weighting with Multi-armed Bandit heuristics
• SPB-MaxSAT-c-FPS
• Combination with ⁴: look-ahead with probabilistic sampling at local optimum
• Results at MSE’24, anytime categories:
• score = Σ_{benchmark i} (1+ cost of best known cost for i) / (1 + cost of solution for i found by s)

​

​

​

​

• Conclusion:
• Band/FPS only slightly improve the performance of plain SPB for unweighted/weighted (0-0.007 score improvement), resp., but
• Both Band and FPS were needed to win 2 of the categories due to the tight competition!

1. Jin, M., He, K., Zheng, J., Xue, J., & Chen, Z., "Combining BandMaxSAT and FPS with SPB-MaxSAT-c," MSE 2024.
2. Zheng, J., Chen, Z., Li, C.-M., & He, K., "Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers," IJCAI 2024.
3. Zheng, J., He, K., Zhou, J., Jin, Y., Li, C. M., & Manya, F., "BandMaxSAT: A Local Search MaxSAT Solver with Multi-armed Bandit," IJCAI 2022.
4. Zheng, J., Zhou, J., He, K., "Farsighted Probabilistic Sampling based Local Search for (Weighted) Partial MaxSAT," AAAI 2023.

Unweighted, 60s

Unweighted, 300s

Weighted, 60s

Weighted, 300s

37

TT-Open-WBO-Inc-2020: the Algorithmics

M := SAT(H)

​

​

M := LocalSearch(M)

Incremental SAT-based Flow

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

TORC polarity selection

Weighted: TSB variable boost

Fallback to LSU?

TORC polarity selection

Weighted: TSB variable boost

​

​

​

​

​

​

​

​

​

​

​

​

​

Polosat became too slow?

Approximation: BMO -- weighted; Mrs. Beaver (OBV) -- unweighted

SAT

Polosat: SAT-based Local Search

SAT

Yes

No

38

TT-Open-WBO-Inc Genealogy

Open-WBO-LSU¹

Open-WBO-Inc-BMO²

Weighted MaxSAT by BMO approximation²

TT-Open-WBO-Inc-2019³

Anytime-MaxSAT-dedicated SAT heuristics⁴

TT-Open-WBO-Inc-2020⁶

• SatLike local search as preprocessing⁵
• Unweighted MaxSAT by OBV approximation (Mrs. Beaver)^4,7
• SAT-based local search (Polosat)⁸

1. Martins, R., Manquinho, V., & Lynce, I., "Open-WBO: A Modular MaxSAT Solver," SAT 2014.
2. Joshi, S., Kumar, P., Rao, S., & Martins, R., "Open-wbo-inc: Approximation strategies for incomplete weighted maxsat," JSAT 2019.
3. Nadel, A., "Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT," JSAT 2020.
4. Nadel, A., "Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization," FMCAD 2019.
5. Cai, S., & Lei, Z., "Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability," AI 2020.
6. Nadel, A., "TT-Open-WBO-Inc: an Efficient Anytime MaxSAT Solver," JSAT 2024.
7. Nadel, A., "Solving MaxSAT with Bit-Vector Optimization," SAT 2018.
8. Nadel, A., "On Optimizing a Generic Function in SAT," FMCAD 2020.
9. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.
10. Chu, Y., Li, C.-M., Ye, F., & Cai, S., "Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme," SAT 2024.
11. Jin, M., He, K., Zheng, J., Xue, J., & Chen, Z., "Combining BandMaxSAT and FPS with SPB-MaxSAT-c," MSE 2024.

​

TT-Open-WBO-Inc

MSE’21-24

SAT&LS solvers integration & Polosat Tuning

Efficient SAT encodings + Linear SAT-UNSAT (LSU) algorithm

SatLike-c⁵

NuWLS-c⁹

NuWLS-c-2023¹⁰

Novelty in local search

SPB-MaxSAT-c*¹¹

39

TT-Open-WBO-Inc

Current Version

• Available at https://github.com/alexander-nadel-academic/tt-open-wbo-inc/
• Two SAT solvers:
• Glucose
• IntelSAT
• Polosat adjustments:
• When update the bad observables?
• Flip only the current bad observable or the whole prefix or both?
• Parameter tuning for MSEs
• Updated to the best performing local search after each MSE
• Yearly results:
• Better than the previous TT-Open-WBO-Inc version
• In top-3 of MSE, but outperformed by the latest and greatest LS & TT-Open-WBO-Inc-20

40

Thanks for your attention!�

41

Linear Search SAT-UNSAT (LSU)¹

42

9/8/2025

The optimal model

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

All the models

100

90

83

60

54

52

49

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

42

���

43

9/8/2025

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

Linear Search SAT-UNSAT (LSU)¹

43

��

44

9/8/2025

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

44

��

45

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

45

��

46

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

46

��

47

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

47

��

48

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

48

��

49

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

49

��

50

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

50

��

51

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

51

��

52

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

52

��

53

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

53

��

54

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

54

��

55

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

55

��

56

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

56

��

57

9/8/2025

1. F 🡨 H (a CNF F is initialized with the hard clauses)
2. Run an incremental SAT solver over F
3. If SAT with a model M
• Block all the models of weight ≥ w(M) in F (using a cardinality or a PB constraint)
4. Else (UNSAT)
• Return the last model M (M is guaranteed to be an optimal model)

90

83

60

54

52

49

100

1. Le Berre, D., & Parrain, A., "The sat4j library, release 2.2," JSAT 2010.

Linear Search SAT-UNSAT (LSU)¹

57

Local Search in MaxSAT

The Shared Algorithmic Framework

58

NuWLS Local Search Algorithm¹

Update Weights at Local Optima

1. Chu, Y., Cai, S., & Luo, C., "NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques," AAAI 2023.

59

Optimization modulo Bitvectors (OBV)

• Input in MaxSAT
• Clauses H (aka, hard clauses)
• Target T = {t_n-1, t_n-2 , … , t₀} weighted by W = {w_n-1, w_n-2 , … , w₀}
• Each t_i is a literal, associated with an integer weight w_i > 0
• Output in MaxSAT
• Solution to H that minimizes w_n-1*t_n-1 + … + w₁*t₁ + … + w₀*t₀

​

by Reduction to MaxSAT

Example: H = (a + b) (a + c) (¬a + ¬c); T = {a,b,c}

H has 3 models: M₁={a=0, b=1, c=1}; M₂={a=1, b=0, c=0}; M₃={a=1, b=1, c=0}

OBV vs. MaxSAT solving: The order makes OBV easier than MaxSAT

60