# Integer Linear Programming Preprocessing for Maximum Satisfiability

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

## Key facts

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

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

- [Optimizing Binary Decision Diagrams with MaxSAT for classification](https://mlsanity.com/paper/2203.11386/) (2022)
- [Clause Vivification by Unit Propagation in CDCL SAT Solvers](https://mlsanity.com/paper/1807.11061/) (2018)
- [BandMaxSAT: A Local Search MaxSAT Solver with Multi-armed Bandit](https://mlsanity.com/paper/2201.05544/) (2022)

## Abstract (arXiv)

The Maximum Satisfiability problem (MaxSAT) is a major optimization challenge with numerous practical applications. In recent MaxSAT evaluations, most MaxSAT solvers have incorporated an Integer Linear Programming (ILP) solver into their portfolios. However, a good portfolio strategy requires a lot of tuning work and is limited to the profiling benchmark. This paper proposes a methodology to fully integrate ILP preprocessing techniques into the MaxSAT solving pipeline and investigates the impact on the top-performing MaxSAT solvers. Experimental results show that our approach helps to improve 5 out of 6 state-of-the-art MaxSAT solvers, especially for WMaxCDCL-OpenWbo1200, the winner of the MaxSAT evaluation 2024 on the unweighted track, which is able to solve 15 additional instances using our methodology.