Resizing cardinality constraints for MaxSAT

Article type: Research Article

Authors: Jahren, Eivind^{a; *} | Asín Achá, Roberto^b

Affiliations: [a] Department of Informatics, University of Bergen, Norway. E-mail: eivind.jahren@ii.uib.no | [b] Computer Science Department, Universidad de Concepción, Chile. E-mail: rasin@udec.cl

Correspondence: [*] Corresponding author. E-mail: eivind.jahren@ii.uib.no.

Abstract: 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.

Keywords: MaxSAT, cardinality encoding

DOI: 10.3233/AIC-180768

Journal: AI Communications, vol. 31, no. 4, pp. 355-367, 2018