Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey,
"Detecting cardinality constraints in CNF"
: Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Serie Lecture Notes in Computer Science (LNCS), Vol. 8561, Springer, Seite(n) 285-301, 2014
Original Titel:
Detecting cardinality constraints in CNF
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14)
Original Kurzfassung:
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.
Forschungs-