1;2c@inproceedings{BergJ:CP2017,
author = {Jeremias Berg and Matti J\"arvisalo},
title = {Weight-Aware Core Extraction in {SAT}-Based {MaxSAT} Solving},
booktitle = {Proceedings of the 23rd International Conference on
             Principles and Practice of Constraint Programming (CP 2017)},
editor = {J. Christopher Beck},
pages = {652--670},
volume = {10416},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
year = {2017},
}

Abstract:

Maximum satisfiability (MaxSAT) is today a competitive approach to
tackling NP-hard optimization problems in a variety of AI and
industrial domains. A great majority of the modern state-of-the-art
MaxSAT solvers are core-guided, relying on a SAT solver to iteratively
extract unsatisfiable cores of the soft clauses in the working formula
and ruling out the found cores via adding cardinality constraints
into the working formula until a solution is found. In this work we
propose weight-aware core extraction (WCE) as a refinement to the
current common approach of core-guided solvers. WCE integrates
knowledge of soft clause weights into the core extraction process, and
allows for delaying the addition of cardinality constraints into the
working formula. We show that WCE noticeably improves in practice the
performance of PMRES, one of the recent core-guided MaxSAT algorithms
using soft cardinality constraints, and explain how the approach can
be integrated into other core-guided algorithms.