# Enhancing Local Search for MaxSAT with Deep Differentiation Clause Weighting

arXiv: https://arxiv.org/abs/2512.05619 · HTML: https://mlsanity.com/paper/2512.05619/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 46 references that are in the map.
- First posted on arXiv 5 Dec 2025.

## Builds on (most cited first, 6 of 6)

- [Learning Features and Abstract Actions for Computing Generalized Plans](https://mlsanity.com/paper/1811.07231/) (2018)
- [BandMaxSAT: A Local Search MaxSAT Solver with Multi-armed Bandit](https://mlsanity.com/paper/2201.05544/) (2022)
- [Incomplete MaxSAT Approaches for Combinatorial Testing](https://mlsanity.com/paper/2105.12552/) (2021)
- [Farsighted Probabilistic Sampling: A General Strategy for Boosting Local Search MaxSAT Solvers](https://mlsanity.com/paper/2108.09988/) (2021)
- [Solving the capacitated vehicle routing problem with timing windows using rollouts and MAX-SAT](https://mlsanity.com/paper/2206.06618/) (2022)
- [Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers](https://mlsanity.com/paper/2401.10589/) (2024)

## Abstract (arXiv)

Partial Maximum Satisfiability (PMS) and Weighted Partial Maximum Satisfiability (WPMS) generalize Maximum Satisfiability (MaxSAT), with broad real-world applications. Recent advances in Stochastic Local Search (SLS) algorithms for solving (W)PMS have mainly focused on designing clause weighting schemes. However, existing methods often fail to adequately distinguish between PMS and WPMS, typically employing uniform update strategies for clause weights and overlooking critical structural differences between the two problem types. In this work, we present a novel clause weighting scheme that, for the first time, updates the clause weights of PMS and WPMS instances according to distinct conditions. This scheme also introduces a new initialization method, which better accommodates the unique characteristics of both instance types. Furthermore, we propose a decimation method that prioritizes satisfying unit and hard clauses, effectively complementing our proposed clause weighting scheme. Building on these methods, we develop a new SLS solver for (W)PMS named DeepDist. Experimental results on benchmarks from the anytime tracks of recent MaxSAT Evaluations show that DeepDist outperforms state-of-the-art SLS solvers. Notably, a hybrid solver combining DeepDist with TT-Open-WBO-Inc surpasses the performance of the MaxSAT Evaluation 2024 winners, SPB-MaxSAT-c-Band and SPB-MaxSAT-c-FPS, highlighting the effectiveness of our approach. The code is available at https://github.com/jmhmaxsat/DeepDist