Detecting Cardinality Constraints in CNF

Abstract : We present novel approaches to detect cardinality constraints\r≠xpressed in CNF. The first approach is based on a syntactic analysis\r\nof specific data structures used in SAT solvers to represent binary and\r\nternary clauses, whereas the second approach is based on a semantic\r\nanalysis by unit propagation. The syntactic approach computes an approximation\r\nof the cardinality constraints AtMost-1 and AtMost-2 constraints\r\nvery fast, whereas the semantic approach has the property to be\r\ngeneric, i.e. it can detect cardinality constraints AtMost-k for any k, at\r\na higher computation cost. Our experimental results suggest that both\r\napproaches are efficient at recovering AtMost-1 and AtMost-2 cardinality\r\nconstraints.