Reduced Cost Fixing for Maximum Satisfiability

Reduced Cost Fixing for Maximum Satisfiability

Fahiem Bacchus, Antti Hyttinen, Matti Järvisalo, Paul Saikko

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Best Sister Conferences. Pages 5209-5213. https://doi.org/10.24963/ijcai.2018/723

Maximum satisfiability (MaxSAT) offers a competitive approach to solving NP-hard real-world optimization problems. While state-of-the-art MaxSAT solvers rely heavily on Boolean satisfiability (SAT) solvers, a recent trend, brought on by MaxSAT solvers implementing the so-called implicit hitting set (IHS) approach, is to integrate techniques from the realm of integer programming (IP) into the solving process. This allows for making use of additional IP solving techniques to further speed up MaxSAT solving. In this line of work, we investigate the integration of the technique of reduced cost fixing from the IP realm into IHS solvers, and empirically show that reduced cost fixing considerable speeds up a state-of-the-art MaxSAT solver implementing the IHS approach.
Keywords:
Constraints and SAT: Constraint Optimisation
Constraints and SAT: MaxSAT, MinSAT