Integer Linear Programming Preprocessing for Maximum Satisfiability
Abstract
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.
Cite
@article{arxiv.2506.06216,
title = {Integer Linear Programming Preprocessing for Maximum Satisfiability},
author = {Jialu Zhang and Chu-Min Li and Sami Cherif and Shuolin Li and Zhifei Zheng},
journal= {arXiv preprint arXiv:2506.06216},
year = {2026}
}