Resizing cardinality constraints for MaxSAT

摘要

In this paper we describe several variations of the incremental MSU3 and MSU4 algorithms for the MaxSAT problem, and show that some of these improve performance. Among the variations considered are new cardinality constraint encodings which enable incrementally updating the constraint, and have smaller worst-case size than those encodings previously considered. The new cardinality encodings are based on the well-known sorting networks. The incremental approach is also extended, in a novel way, inspired by the idea behind resizing arrays. Best performance was achieved when the totalizer encoding was used in conjunction with sorting networks; unlike other implementations of such combinations in the literature we found that to get best performance, sorting networks should be used very sparingly. We submitted a solver using a version of the methods described in this paper to the 2017 MaxSAT evaluation where it placed fourth out of 8 solvers participating in the unweighted category.