Open-WBO-Inc: Approximation Strategies for Incomplete Weighted MaxSAT

Abstract

Incomplete MaxSAT solving aims to quickly find a solution that attempts to minimize the sum of the weights of unsatisfied soft clauses without providing any optimality guarantees. In this paper, we propose two approximation strategies for improving incomplete weighted MaxSAT solving. In one of the strategies, we cluster the weights and approximate them with a representative weight. In another strategy, we break up the problem of minimizing the sum of weights of unsatisfiable clauses into multiple minimization subproblems. We have implemented these strategies in a tool Open-WBO-Inc. Using the subproblem minimization strategy, Open-WBO-Inc placed first and second in the weighted incomplete tracks in the MaxSAT Evaluation 2018 whereas the strategy based on weight approximation was placed fourth. We compare these strategies with the best incomplete MaxSAT solvers on benchmarks taken from MaxSAT Evaluation 2017 and MaxSAT Evaluation 2018 and show that the strategies proposed are competitive with the best of the solvers.