Weight-Aware Transformations for MaxSAT

Abstract

The core-guided MAXSAT algorithms are one of the most successful approaches for solving MAXSAT problems. Several of these algorithms are based on the idea of core relaxation, where all clauses in the core must have the same weight. For weighted instances, such cores are obtained by using cloning clauses whose weights are larger than the minimum weight. While cloning is widely used, the question of whether it is necessary has only recently been raised. We investigate this question and propose a novel core transformation procedure that takes weights structure into account. In particular, we consider two MAXSAT algorithms, OLL and MAXRES, and show how they can be made weight-aware; we can reuse internal encoding variables in the case of OLL and exploit the MAXSAT resolution rule in the case of MAXRES. We implemented our algorithm on top of OLL with sequential counters encoding of cardinality constraints and show that it has competitive performance compared to this baseline. Moreover, there are several families of benchmarks where it significantly outperforms the baseline.