Sciweavers

SAT
2009
Springer

Cardinality Networks and Their Applications

13 years 11 months ago
Cardinality Networks and Their Applications
We introduce Cardinality Networks, a new CNF encoding of cardinality constraints. It improves upon the previously existing encodings such as the sorting networks of [ES06] in that it requires much less clauses and auxiliary variables, while arc consistency is still preserved: e.g., for a constraint x1 + . . . + xn ≤ k, as soon as k variables among the xi’s become true, unit propagation sets all other xi’s to false. Our encoding also still admits incremental strengthening: this constraint for any smaller k is obtained without adding any new clauses, by setting a single variable to false. Here we give precise recursive definitions of the clause sets that are needed and give detailed proofs of the required properties. We demonstrate the practical impact of this new encoding by careful experiments comparing it with previous encodings on real-world instances.
Roberto Asín, Robert Nieuwenhuis, Albert Ol
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SAT
Authors Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Comments (0)