Reduced Cost Fixing for Maximum Satisfiability
Abstract
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.
Cite
Text
Bacchus et al. "Reduced Cost Fixing for Maximum Satisfiability." International Joint Conference on Artificial Intelligence, 2018. doi:10.24963/IJCAI.2018/723Markdown
[Bacchus et al. "Reduced Cost Fixing for Maximum Satisfiability." International Joint Conference on Artificial Intelligence, 2018.](https://mlanthology.org/ijcai/2018/bacchus2018ijcai-reduced/) doi:10.24963/IJCAI.2018/723BibTeX
@inproceedings{bacchus2018ijcai-reduced,
title = {{Reduced Cost Fixing for Maximum Satisfiability}},
author = {Bacchus, Fahiem and Hyttinen, Antti and Järvisalo, Matti and Saikko, Paul},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2018},
pages = {5209-5213},
doi = {10.24963/IJCAI.2018/723},
url = {https://mlanthology.org/ijcai/2018/bacchus2018ijcai-reduced/}
}