Counting Solutions Under Cardinality Constraints: Structure Counts in Counting

Model counting is a powerful extension of constraint reasoning that, instead of finding a solution to a constraint system, allows to identify the number of such solutions. Cardinality constraints are used to filter solutions of a certain quality by restricting the number of elements that can be added to the solution. Naturally, one would like to combine both in order to count the number of solutions of good quality. Unfortunately, the two concepts do not get along so well as (1) cardinality constraints may not be parsimonious (due to auxiliary variables, the system’s number of solutions may change in an uncontrolled way) and (2) such constraints may destroy structural properties, which are crucial for the performance of modern solvers. This article provides a systematic study of existing cardinality constraints in the light of model counting, observing that none of them are both, parsimonious and treewidth-preserving. We present structure-aware cardinality constraints that are parsimonious and guaranteed to increase the input’s treewidth only in a controlled way. Detailed experiments reveal that our encodings outperform existing ones.