Approximation Strategies for Incomplete MaxSAT
This work addresses the need for faster, approximate solutions in MaxSAT solving, which is incremental as it builds on existing incomplete methods.
The paper tackles the problem of incomplete MaxSAT solving by proposing two approximation strategies—clustering weights and breaking the problem into subproblems—to quickly find solutions that minimize unsatisfied clause weights, with experimental results showing they outperform the best incomplete solvers from the MaxSAT Evaluation 2017.
Incomplete MaxSAT solving aims to quickly find a solution that attempts to minimize the sum of the weights of the unsatisfied soft clauses without providing any optimality guarantees. In this paper, we propose two approximation strategies for improving incomplete 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. Experimental results show that approximation strategies can be used to find better solutions than the best incomplete solvers in the MaxSAT Evaluation 2017.