TY - GEN
T1 - Detecting cardinality constraints in CNF
AU - Biere, Armin
AU - Le Berre, Daniel
AU - Lonca, Emmanuel
AU - Manthey, Norbert
PY - 2014
Y1 - 2014
N2 - 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 in SAT solvers 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 both
approaches are efficient at recovering AtMost-1 and AtMost-2 cardinality
constraints.
AB - 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 in SAT solvers 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 both
approaches are efficient at recovering AtMost-1 and AtMost-2 cardinality
constraints.
UR - https://www.scopus.com/pages/publications/84958539047
U2 - 10.1007/978-3-319-09284-3_22
DO - 10.1007/978-3-319-09284-3_22
M3 - Conference proceedings
VL - 8561
T3 - Lecture Notes in Computer Science (LNCS)
SP - 285
EP - 301
BT - Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14)
PB - Springer
ER -