Exploiting Resolution-based Representations for MaxSAT Solving

TL;DR

This paper introduces a novel resolution-based graph partitioning approach for MaxSAT solving, improving the efficiency and scalability of existing algorithms on industrial instances.

Contribution

It proposes a new partitioning method using resolution-based graphs and a proximity measure to enhance MaxSAT solver performance.

Findings

Outperforms existing MaxSAT solvers on industrial benchmarks.

Effectively finds optimal solutions for larger and more complex instances.

Demonstrates the benefit of graph-based partitioning in MaxSAT algorithms.

Abstract

Most recent MaxSAT algorithms rely on a succession of calls to a SAT solver in order to find an optimal solution. In particular, several algorithms take advantage of the ability of SAT solvers to identify unsatisfiable subformulas. Usually, these MaxSAT algorithms perform better when small unsatisfiable subformulas are found early. However, this is not the case in many problem instances, since the whole formula is given to the SAT solver in each call. In this paper, we propose to partition the MaxSAT formula using a resolution-based graph representation. Partitions are then iteratively joined by using a proximity measure extracted from the graph representation of the formula. The algorithm ends when only one partition remains and the optimal solution is found. Experimental results show that this new approach further enhances a state of the art MaxSAT solver to optimally solve a larger set of industrial problem instances.