Google Research

Exploiting the Structure of Unsatisfiable Cores in MaxSAT

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI (2015), pp. 283-289

Abstract

We propose a new approach that exploits the good properties of core-guided and model-guided MaxSAT solvers. In particular, we show how to effectively exploit the structure of unsatisfiable cores in MaxSAT instances. Experimental results on industrial instances show that the proposed approach outperforms both complete and incomplete state-of-the-art MaxSAT solvers at the last international MaxSAT Evaluation in terms of robustness and total number of solved instances.

Learn more about how we do research

We maintain a portfolio of research projects, providing individuals and teams the freedom to emphasize specific types of work