Detecting cardinality constraints in CNF

ABSTRACT. We present novel approaches to detect cardinality constraints expressed in CNF. The first approach is based on a syntactic analysis of specific data structures used to represent binary and ternary clauses, whereas the second approach is based on a semantic analysis by unit propagation.

The syntactic approach computes an approximation of the cardinality constraints AtMost-$1$ and AtMost-$2$ constraints very fast, whereas the semantic approach has the property to be generic, i.e. it can detect cardinality constraints AtMost-$k$ for any $k$, at a higher computation cost.

Our experimental results suggest that the syntactic approach is efficient at recovering AtMost-$1$ and that the semantic one is efficient at recovering AtMost-$2$ cardinality constraints.