DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2026.23

Near-Optimal Encodings of Cardinality Constraints

Authors: Andrew Krapivin, Benjamin Przybocki, and Bernardo Subercaseaux

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{krapivin_et_al:LIPIcs.SAT.2026.23,
  author =	{Krapivin, Andrew and Przybocki, Benjamin and Subercaseaux, Bernardo},
  title =	{{Near-Optimal Encodings of Cardinality Constraints}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.23},
  URN =		{urn:nbn:de:0030-drops-263294},
  doi =		{10.4230/LIPIcs.SAT.2026.23},
  annote =	{Keywords: CNF encodings, cardinality constraints, circuit complexity}
}

Search Results

Documents authored by Krapivin, Andrew

Near-Optimal Encodings of Cardinality Constraints

Abstract

Cite as

Thanks for your feedback!

Could not send message