Integer Linear Programming Preprocessing for Maximum Satisfiability

TL;DR

This paper introduces a methodology to incorporate ILP preprocessing into MaxSAT solvers, significantly enhancing their performance on benchmark instances, especially for the top solver in recent evaluations.

Contribution

It presents a novel approach to fully integrate ILP preprocessing techniques into MaxSAT solving pipelines, improving solver effectiveness without extensive tuning.

Findings

Improved performance on 5 out of 6 top MaxSAT solvers.

Enabled the winning solver of MaxSAT 2024 to solve 15 more instances.

Demonstrated the effectiveness of ILP preprocessing in MaxSAT solving.

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.