Large Neighbourhood Search for Anytime MaxSAT Solving

Large Neighbourhood Search for Anytime MaxSAT Solving

Randy Hickey, Fahiem Bacchus

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence
Main Track. Pages 1818-1824. https://doi.org/10.24963/ijcai.2022/253

Large Neighbourhood Search (LNS) is an algorithmic framework for optimization problems that can yield good performance in many domains. In this paper, we present a method for applying LNS to improve anytime maximum satisfiability (MaxSAT) solving by introducing a neighbourhood selection policy that shows good empirical performance. We show that our LNS solver can often improve the suboptimal solutions produced by other anytime MaxSAT solvers. When starting with a suboptimal solution of reasonable quality, our approach often finds a better solution than the original anytime solver can achieve. We demonstrate that implementing our LNS solver on top of three different state-of-the-art anytime solvers improves the anytime performance of all three solvers within the standard time limit used in the incomplete tracks of the annual MaxSAT Evaluation.
Keywords:
Constraint Satisfaction and Optimization: Satisfiabilty
Constraint Satisfaction and Optimization: Solvers and Tools