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}
}

Document

DOI: 10.4230/LIPIcs.SAT.2026.29

Automated Reencoding Meets Graph Theory

Authors: Benjamin Przybocki, Bernardo Subercaseaux, and Marijn J. H. Heule

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

Abstract

Bounded Variable Addition (BVA) is a central preprocessing method in modern state-of-the-art SAT solvers. We provide a graph-theoretic characterization of which 2-CNF encodings can be constructed by an idealized BVA algorithm. Based on this insight, we prove new results about the behavior and limitations of BVA and its interaction with other preprocessing techniques. We show that idealized BVA, plus some minor additional preprocessing (e.g., equivalent literal substitution), can reencode any 2-CNF formula with n variables into an equivalent 2-CNF formula with (lg(3)/4 + o(1)) n²/(lg n) clauses. Furthermore, we show that without the additional preprocessing the constant factor worsens from lg(3)/4 ≈ 0.396 to 1, and that no reencoding method can achieve a constant below 0.25. On the other hand, for the at-most-one constraint on n variables, we prove that idealized BVA cannot reencode this constraint using fewer than 3n-6 clauses, a bound that we prove is achieved by actual implementations. In particular, this shows that the product encoding for at-most-one, which uses 2n+o(n) clauses, cannot be constructed by BVA regardless of the heuristics used. Finally, our graph-theoretic characterization of BVA allows us to leverage recent work in algorithmic graph theory to develop a drastically more efficient implementation of BVA that achieves a comparable clause reduction on random monotone 2-CNF formulas.

Cite as

Benjamin Przybocki, Bernardo Subercaseaux, and Marijn J. H. Heule. Automated Reencoding Meets Graph Theory. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{przybocki_et_al:LIPIcs.SAT.2026.29,
  author =	{Przybocki, Benjamin and Subercaseaux, Bernardo and Heule, Marijn J. H.},
  title =	{{Automated Reencoding Meets Graph Theory}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{29:1--29: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.29},
  URN =		{urn:nbn:de:0030-drops-263358},
  doi =		{10.4230/LIPIcs.SAT.2026.29},
  annote =	{Keywords: SAT solving, CNF encodings, BVA, Rectifier networks}
}

Search Results

Documents authored by Przybocki, Benjamin

Near-Optimal Encodings of Cardinality Constraints

Abstract

Cite as

Automated Reencoding Meets Graph Theory

Abstract

Cite as

Thanks for your feedback!

Could not send message