caa a22 4500 445879343 CHVBK 20180317145537.0 cr unu---uuuuu 170323e20110401xx s 000 0 eng 10.1007/s10601-010-9105-0 doi (NATIONALLICENCE)springer-10.1007/s10601-010-9105-0 Cardinality Networks: a theoretical and empirical study [Elektronische Daten] [Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell] We introduce Cardinality Networks, a new CNF encoding of cardinality constraints. It improves upon the previously existing encodings such as the sorting networks of Eén and Sörensson (JSAT 2:1-26, 2006) 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. Springer Science+Business Media, LLC, 2011 SAT nationallicence Cardinality constraints nationallicence SAT encodings nationallicence Asín Roberto Technical University of Catalonia, Barcelona, Spain aut Nieuwenhuis Robert Technical University of Catalonia, Barcelona, Spain aut Oliveras Albert Technical University of Catalonia, Barcelona, Spain aut Rodríguez-Carbonell Enric Technical University of Catalonia, Barcelona, Spain aut Constraints Springer US; http://www.springer-ny.com 16/2(2011-04-01), 195-221 1383-7133 16:2<195 2011 16 10601 https://doi.org/10.1007/s10601-010-9105-0 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10601-010-9105-0 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Asín Roberto Technical University of Catalonia, Barcelona, Spain aut NATIONALLICENCE 700 1- Nieuwenhuis Robert Technical University of Catalonia, Barcelona, Spain aut NATIONALLICENCE 700 1- Oliveras Albert Technical University of Catalonia, Barcelona, Spain aut NATIONALLICENCE 700 1- Rodríguez-Carbonell Enric Technical University of Catalonia, Barcelona, Spain aut NATIONALLICENCE 773 0- Constraints Springer US; http://www.springer-ny.com 16/2(2011-04-01), 195-221 1383-7133 16:2<195 2011 16 10601 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer