On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving

Abstract

In recent years, unsatisfiability-based algorithms have become prevalent as state of the art for solving industrial instances of Maximum Satisfiability (MaxSAT). These algorithms perform a succession of unsatisfiable SAT solver calls until an optimal solution is found. In several of these algorithms, cardinality or pseudo-Boolean constraints are extended between iterations. However, in most cases, the formula provided to the SAT solver in each iteration must be rebuilt and no knowledge is reused from one iteration to the next.

This paper describes how to implement incremental unsatisfiability-based algorithms for MaxSAT. In particular, we detail and analyze our implementation of the MSU3 algorithm in the open-wbo framework that performed remarkably well in the MaxSAT Evaluation of 2014. Furthermore, we also propose to extend incrementality to weighted MaxSAT through an incremental encoding of pseudo-Boolean constraints. The experimental results show that the performance of MaxSAT algorithms can be greatly improved by exploiting the learned information and maintaining the internal state of the SAT solver between iterations. Finally, the proposed incremental encodings of cardinality and pseudo-Boolean constraints are not exclusive for MaxSAT usage and can be used in other domains.