Open-WBO-Inc Incomplete MaxSAT Solver

Open-WBO-Inc is a MaxSAT solver tailored to the incomplete MaxSAT problem. In incomplete MaxSAT, the goal is to find an approximate solution to a given MaxSAT formula in very little time. Open-WBO-Inc uses various approximation techniques, such as those that reduce encoding sizes, to find a solution close to the optimal in much lesser time than would otherwise be needed. Open-WBO-Inc is based on Open-WBO, a state-of-the-art MaxSAT solver, and has been implemented in C++.

Motivation

In the weighted MaxSAT problem, the input consists of a set of clauses and positive integral weights associated with each clause. The goal is to obtain an assignment of variables that minimizes the cost (sum of unsatisfied weights) of the formula. The weighted MaxSAT problem typically involves encoding a pseudo-boolean (PB) constraint in the CNF form to constrain the number of clauses that may be unsatisfied in a given iteration of the solution search process. The number of clauses added for this encoding could often be a large fraction of the resulting formula size. As a result, having a large encoding increases the time needed to find the solution. One of the best performing encodings, GTE, can generate an exponential number of clauses in the size of the PB constraint in the worst case, which is when the number of unique weights are very high. However, for many applications, it might be sufficient to obtain an approximate solution while greatly speeding up the search.

Approach

We proposed two approximation algorithms:

apx-weight (Open-WBO-Inc-Cluster)

This algorithm aims to reduce the size of the encoding, thus reducing the search time. A key observation is that the size of the GTE encoding increases based on the number of distinct weights in the formula. If this could be reduced, the encoding size would also reduce. We achieve this by clustering the weights to a small number of clusters using divisive hierarchical clustering. In each cluster, all the weights are replaced by a representative weight, such as their mean. As a result, the number of unique weights now reduces to the number of clusters. Clustering $n$ weights to $k$ clusters can be done in $\mathcal O(nk)$ time, which was observed to be negligible compared to the total time taken by the solver.

apx-subprob (Open-WBO-Inc-BMO)

This extends the ideas in apx-weight. Once the clusters are obtained, the clauses in the formula are arranged in the descending order of their weights. Then, iterating from the largest representative weight to the smallest, the formula in each cluster is solved. Once an optimum is obtained for any cluster, it is fixed, and no further relaxation is made when operating over subsequent clusters. This breaks the problem into multiple subproblems, effectively enforcing the boolean multilevel optimization (BMO) condition. This can often be an effective strategy because many real-world MaxSAT formulae might have weights that satisfy the BMO assumption.

Results

Both algorithms outperformed most of the existing state-of-the-art incomplete MaxSAT solvers. In particular, apx-subprob outperformed maxroster, which was the best performing solver in the MaxSAT Evaluation 2017.

In the MaxSAT Evaluation 2018, apx-subprob in Open-WBO-Inc secured the first position in the 60 seconds category and the second position in the 300 seconds category in the weighted incomplete MaxSAT track. apx-weight secured the fourth position in both these categories.