Incremental Cardinality Constraints for MaxSAT
This work addresses performance issues in MaxSAT solving for researchers and practitioners, though it is incremental in nature.
The paper tackled the inefficiency of non-incremental MaxSAT algorithms by introducing incremental schemes for cardinality constraints, resulting in a significant performance boost for these algorithms compared to their non-incremental counterparts.
Maximum Satisfiability (MaxSAT) is an optimization variant of the Boolean Satisfiability (SAT) problem. In general, MaxSAT algorithms perform a succession of SAT solver calls to reach an optimum solution making extensive use of cardinality constraints. Many of these algorithms are non-incremental in nature, i.e. at each iteration the formula is rebuilt and no knowledge is reused from one iteration to another. In this paper, we exploit the knowledge acquired across iterations using novel schemes to use cardinality constraints in an incremental fashion. We integrate these schemes with several MaxSAT algorithms. Our experimental results show a significant performance boost for these algo- rithms as compared to their non-incremental counterparts. These results suggest that incremental cardinality constraints could be beneficial for other constraint solving domains.