Document Open Access Logo

Near-Optimal Encodings of Cardinality Constraints

Authors Andrew Krapivin , Benjamin Przybocki , Bernardo Subercaseaux

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.23.pdf
  • Filesize: 1.14 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Theory of computation → Automated reasoning
  • Theory of computation → Circuit complexity
Keywords
  • CNF encodings
  • cardinality constraints
  • circuit complexity

Metrics

Abstract

We present several novel encodings for cardinality constraints, which use fewer clauses than previous encodings and, more importantly, introduce new generally applicable techniques for constructing compact encodings. First, we present a CNF encoding for the AtMostOne(x_1,…,x_n) constraint using 2n + 2 √{2n} + O(∛n) clauses, thus refuting the conjectured optimality of Chen’s product encoding. Our construction also yields a smaller monotone circuit for the threshold-2 function, improving on a 50-year-old construction of Adleman and incidentally solving a long-standing open problem in circuit complexity. On the other hand, we show that any encoding for this constraint requires at least 2n + √{n+1} - 2 clauses, which is the first nontrivial unconditional lower bound for this constraint and answers a question of Kučera, Savický, and Vorel. We then turn our attention to encodings of AtMost_k(x_1,…,x_n), where we introduce grid compression, a technique inspired by hash tables, to give encodings using 2n + o(n) clauses as long as k = o(∛{n}) and 4n + o(n) clauses as long as k = o(n). Previously, the smallest known encodings were of size (k+1)n + o(n) for k ≤ 5 and 7n - o(n) for k ≥ 6.

Cite As Get BibTex

Andrew Krapivin, Benjamin Przybocki, and Bernardo Subercaseaux. Near-Optimal Encodings of Cardinality Constraints. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.23

Author Details

Andrew Krapivin
  • Carnegie Mellon University, Pittsburgh, PA, USA
Benjamin Przybocki
  • Carnegie Mellon University, Pittsburgh, PA, USA
Bernardo Subercaseaux
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

  • Krapivin, Andrew: Krapivin was supported by the NSF grant CNS2504471, Packard Foundation grant 2020-71730, and the Jeanne B. and Richard F. Berdik ARCS Pittsburgh Endowed Scholar Award.
  • Przybocki, Benjamin: Przybocki was supported by NSF grant DMS-2434625 and the NSF Graduate Research Fellowship Program under Grant No. DGE-2140739.
  • Subercaseaux, Bernardo: Subercaseaux was supported by NSF grant DMS-2434625.

Acknowledgements

We are grateful to Petr Savický for finding an error in an earlier version of this paper. We also thank Marijn Heule for his suggestions on improving the presentation of this paper.

References

  1. Scott Aaronson. P?=NP. In John Forbes Nash, Jr. and Michael Th. Rassias, editors, Open Problems in Mathematics, pages 1-122. Springer International Publishing, 2016. URL: https://doi.org/10.1007/978-3-319-32162-2_1.
  2. Miklós Ajtai, János Komlós, and Endre Szemerédi. Sorting in c log n parallel steps. Combinatorica, 3(1):1-19, 1983. URL: https://doi.org/10.1007/BF02579338.
  3. Kazuyuki Amano and Akira Maruoka. The monotone circuit complexity of quadratic boolean functions. Algorithmica, 46(1):3-14, 2006. URL: https://doi.org/10.1007/s00453-006-0073-0.
  4. Carlos Ansótegui and Felip Manyà. Mapping problems with finite-domain variables to problems with boolean variables. In Holger H. Hoos and David G. Mitchell, editors, Theory and Applications of Satisfiability Testing, pages 1-15. Springer Berlin Heidelberg, 2005. Google Scholar
  5. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks: a theoretical and empirical study. Constraints, 16(2):195-221, 2011. URL: https://doi.org/10.1007/S10601-010-9105-0.
  6. Olivier Bailleux and Yacine Boufkhad. Efficient CNF encoding of boolean cardinality constraints. In Francesca Rossi, editor, Principles and Practice of Constraint Programming - CP, volume 2833 of Lecture Notes in Computer Science, pages 108-122. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45193-8_8.
  7. Yael Ben-Haim, Alexander Ivrii, Oded Margalit, and Arie Matsliah. Perfect hashing and CNF encodings of cardinality constraints. In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT, volume 7317 of Lecture Notes in Computer Science, pages 397-409. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_30.
  8. Peter Anthony Bloniarz. The complexity of monotone boolean functions and an algorithm for finding shortest paths on a graph. PhD thesis, Massachusetts Institute of Technology, 1979. Google Scholar
  9. Lucas Bordeaux and Joao Marques-Silva. Knowledge Compilation with Empowerment. In Mária Bieliková, Gerhard Friedrich, Georg Gottlob, Stefan Katzenbeisser, and György Turán, editors, SOFSEM 2012: Theory and Practice of Computer Science, pages 612-624. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-27660-6_50.
  10. Siegfried Bublitz. Decomposition of graphs and monotone formula size of homogeneous functions. Acta Inform., 23(6):689-696, 1986. URL: https://doi.org/10.1007/BF00264314.
  11. Jingchao Chen. A new SAT encoding of the at-most-one constraint. In Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation, 2010. URL: https://pierre-flener.github.io/research/ModRef10/papers/Jingchao%20Chen.%20A%20New%20SAT%20Encoding%20of%20the%20At-Most-One%20Constraint%20-%20ModRef%202010.pdf.
  12. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to algorithms. MIT Press, Cambridge, MA, third edition, 2009. Google Scholar
  13. Paul E. Dunne. Techniques for the analysis of monotone Boolean networks. PhD thesis, University of Warwick, 1984. Google Scholar
  14. Niklas Eén and Niklas Sörensson. Translating pseudo-boolean constraints into SAT. J. Satisf. Boolean Model. Comput., 2(1-4):1-26, 2006. URL: https://doi.org/10.3233/SAT190014.
  15. Gregory Emdin, Alexander S. Kulikov, Ivan Mihajlin, and Nikita Slezkin. CNF encodings of symmetric functions. Theory Comput. Syst., 68(5):1291-1311, 2024. URL: https://doi.org/10.1007/S00224-024-10168-W.
  16. Paul Erdős, Peter Frankl, and Zoltán Füredi. Families of finite sets in which no set is covered by the union of r others. Israel J. Math., 51(1-2):79-89, 1985. URL: https://doi.org/10.1007/BF02772959.
  17. Alan M. Frisch and Paul A. Giannaros. SAT encodings of the at-most-k constraint: Some old, some new, some fast, some slow. In Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation, 2010. Google Scholar
  18. Ian P. Gent. Arc consistency in SAT. In Frank van Harmelen, editor, Proceedings of the 15th European Conference on Artificial Intelligence, ECAI'2002, Lyon, France, July 2002, pages 121-125. IOS Press, 2002. Google Scholar
  19. Ian P. Gent and Peter Nightingale. A new encoding of AllDifferent into SAT. In International Workshop on Modelling and Reformulating Constraint Satisfaction, volume 3, pages 95-110, 2004. Google Scholar
  20. Mikhail I. Grinchuk. On the monotone complexity of threshold functions. Metody Diskret. Anal., 52:41-48, 120, 1992. Google Scholar
  21. Thaís Bardini Idalino and Lucia Moura. A Survey of Cover-Free Families: Constructions, Applications, and Generalizations, pages 195-239. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-48679-1_11.
  22. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In SAT, pages 428-437, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
  23. Stasys Jukna. Disproving the single level conjecture. SIAM J. Comput., 36(1):83-98, 2006. URL: https://doi.org/10.1137/S0097539705447001.
  24. Michał Karpiński. CNF Encodings of Cardinality Constraints Based on Comparator Networks. PhD thesis, University of Wrocław, 2019. URL: https://arxiv.org/abs/1911.00586.
  25. William Kautz and Richard Singleton. Nonrandom binary superimposed codes. IEEE Transactions on Information Theory, 10(4):363-377, 1964. URL: https://doi.org/10.1109/TIT.1964.1053689.
  26. Andrew Krapivin, Benjamin Przybocki, and Bernardo Subercaseaux. Near-optimal encodings of cardinality constraints, 2026. URL: https://doi.org/10.48550/arXiv.2603.28954.
  27. Rafail E. Krichevskii. Complexity of contact circuits realizing a function of logical algebra. Sov. Phys. Dokl., 8:770-772, 1964. Google Scholar
  28. Petr Kučera and Petr Savický. Bounds on the size of PC and URC formulas. Journal of Artificial Intelligence Research, 69:1395-1420, December 2020. URL: http://dx.doi.org/10.1613/jair.1.12006, URL: https://doi.org/10.1613/jair.1.12006.
  29. Petr Kučera, Petr Savický, and Vojtěch Vorel. A lower bound on CNF encodings of the at-most-one constraint. Theor. Comput. Sci., 762:51-73, 2019. URL: https://doi.org/10.1016/J.TCS.2018.09.003.
  30. Katja Lenz and Ingo Wegener. The conjunctive complexity of quadratic boolean functions. Theoret. Comput. Sci., 81(2):257-268, 1991. URL: https://doi.org/10.1016/0304-3975(91)90194-7.
  31. João Marques-Silva and Inês Lynce. Towards robust CNF encodings of cardinality constraints. In Christian Bessiere, editor, Principles and Practice of Constraint Programming - CP, volume 4741 of Lecture Notes in Computer Science, pages 483-497. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_35.
  32. Roland Mirwald and Claus P. Schnorr. The multiplicative complexity of quadratic boolean forms. Theoret. Comput. Sci., 102(2):307-328, 1992. URL: https://doi.org/10.1016/0304-3975(92)90235-8.
  33. Van-Hau Nguyen, Van-Quyet Nguyen, Kyungbaek Kim, and Pedro Barahona. Empirical study on SAT-encodings of the at-most-one constraint. In SMA 2020: The 9th International Conference on Smart Media and Applications, Jeju, Republic of Korea, September 17 - 19, 2020, pages 470-475. ACM, 2020. URL: https://doi.org/10.1145/3426020.3426170.
  34. Joseph E. Reeves. Cardinality Constraints in Boolean Satisfiability Solving. PhD thesis, Carnegie Mellon University, 2025. Google Scholar
  35. Igor S. Sergeev. On the complexity of monotone circuits for threshold symmetric boolean functions. Diskret. Mat., 32(1):81-109, 2020. URL: https://doi.org/10.4213/dm1547.
  36. Carsten Sinz. Towards an optimal CNF encoding of boolean cardinality constraints. In Peter van Beek, editor, Principles and Practice of Constraint Programming - CP, volume 3709 of Lecture Notes in Computer Science, pages 827-831. Springer, 2005. URL: https://doi.org/10.1007/11564751_73.
  37. Joost P. Warners. A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2):63-69, October 1998. URL: https://doi.org/10.1016/s0020-0190(98)00144-6.
  38. Ingo Wegener. The complexity of Boolean functions. John Wiley & Sons, Inc., 1987. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact