Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Anbulagan, & Grastien, A. (2009). Importance of variables semantic in CNF encoding of cardinality constraints. In V. Bulitko, & J. C. Beck (Eds.), Eighth symposium on abstraction, reformulation, and approximation, SARA’09. Menlo Park: AAAI.
Bailleux, O., & Boufkhad, Y. (2003). Efficient CNF encoding of Boolean cardinality constraints. In F. Rossi (Ed.), Principles and practice of constraint programming, 9th international conference, CP’03. Lecture notes in computer science (Vol. 2833, pp. 108–122). New York: Springer.
Bailleux, O., Boufkhad, Y., & Roussel, O. (2006). A translation of pseudo Boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation, JSAT, 2(1–4), 191–200.
Bailleux, O., Boufkhad, Y., & Roussel, O. (2009). New encodings of pseudo-Boolean constraints into CNF. In O. Kullmann (Ed.), 12th international conference on theory and applications of satisfiability testing, SAT’09. Lecture notes in computer science (Vol. 5584, pp. 181–194). New York: Springer.
Batcher, K. E. (1968). Sorting networks and their applications. In AFIPS spring joint computing conference (pp. 307–314).
Biere, A. (2010). Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical report, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2010. Technical report 10/1, August 2010, FMV Reports Series.
Büttner, M., & Rintanen, J. (2005). Satisfiability planning with constraints on the number of actions. In S. Biundo, K. L. Myers, & K. Rajan (Eds.), 15th international conference on automated planning and scheduling, ICAPS’05 (pp. 292–299). Menlo Park: AAAI.
Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, CACM, 5(7), 394–397.
Eén, N., & Biere, A. (2005). Effective preprocessing in SAT through variable and clause elimination. In F. Bacchus, & T. Walsh (Eds.), 8th international conference on theory and applications of satisfiability testing, SAT’05. Lecture notes in computer science (Vol. 3569, pp. 61–75). New York: Springer.
Eén, N., & Sörensson, N. (2006). Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2, 1–26.
Marques-Silva, J., & Planes, J. (2008). Algorithms for maximum satisfiability using unsatisfiable cores. In 2008 conference on design, automation and test in Europe conference, DATE’08 (pp. 408–413). Los Alamitos: IEEE Computer Society.
Marques-Silva, J. P., & Lynce, I. (2007). Towards robust cnf encodings of cardinality constraints. In C. Bessiere (Ed.), Principles and practice of constraint programming, 13th international conference, CP’07. Lecture notes in computer science (Vol. 4741, pp. 483–497). New York: Springer.
Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2006). Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). Journal of the ACM, JACM, 53(6), 937–977.
Sinz, C. (2005). Towards an optimal CNF encoding of boolean cardinality constraints. In P. v. Beek (Ed.), Principles and practice of constraint programming, 11th international conference, CP’05. Lecture notes in computer science (Vol. 3709, pp. 827–831). New York: Springer.
Warners, J. P. (1998). A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2), 63–69.
Author information
Authors and Affiliations
Corresponding author
Additional information
All authors partially supported by Spanish Ministry of Education and Science through the LogicTools-2 project (TIN2007-68093-C02-01). The first author is also partially supported by FPI grant TIN2004-03382.
Rights and permissions
About this article
Cite this article
Asín, R., Nieuwenhuis, R., Oliveras, A. et al. Cardinality Networks: a theoretical and empirical study. Constraints 16, 195–221 (2011). https://doi.org/10.1007/s10601-010-9105-0
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10601-010-9105-0