Rights accessRestricted access - publisher's policy
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 x 1 + ... + x n ≤ k, as soon as k variables among the x i ’s become true, unit propagation sets all other x i ’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.
CitationAsín, R.J. [et al.]. Cardinality networks and their applications. A: International Conference on Theory and Applications of Satisfiability Testing. "12th International Conference on Theory and Applications of Satisfiability Testing". Springer, 2009, p. 167-180.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder. If you wish to make any use of the work not provided for in the law, please contact: email@example.com