pith. sign in

arxiv: 2603.28954 · v2 · submitted 2026-03-30 · 💻 cs.CC · cs.LO

Near-Optimal Encodings of Cardinality Constraints

Andrew Krapivin , Benjamin Przybocki , Bernardo Subercaseaux This is my paper

Pith reviewed 2026-05-14 00:30 UTC · model grok-4.3

classification 💻 cs.CC cs.LO
keywords cardinality constraintsCNF encodingAtMostOneAtMost_kmonotone circuitslower boundsgrid compressionSAT
0
0 comments X

The pith

A CNF encoding for AtMostOne uses 2n + 2√(2n) + O(n^{1/3}) clauses, refuting the conjectured optimality of Chen's product encoding.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces new CNF encodings for cardinality constraints that require fewer clauses than prior constructions. For the AtMostOne constraint it gives an explicit encoding with 2n + 2√(2n) + O(n^{1/3}) clauses and proves that every encoding needs at least 2n + √(n+1) - 2 clauses. The same construction produces a smaller monotone circuit for the threshold-2 function than the one known for fifty years. For the general AtMost_k constraint a new grid-compression method yields 2n + o(n) clauses whenever k = o(n^{1/3}) and 4n + o(n) clauses whenever k = o(n). These results improve the best-known upper and lower bounds for both the one-sided and the general case.

Core claim

The central discovery is an explicit CNF encoding of AtMostOne(x1,…,xn) that uses only 2n + 2√(2n) + O(∛n) clauses, together with a matching-style lower bound of 2n + √(n+1) − 2 clauses that any encoding must obey. The same technique yields a monotone circuit for the threshold-2 function smaller than Adleman's construction. For AtMost_k the authors introduce grid compression, a hash-table-inspired compression of the auxiliary variables, to obtain encodings of size 2n + o(n) for k = o(n^{1/3}) and 4n + o(n) for k = o(n).

What carries the argument

Grid compression, a technique that compresses the representation of admissible assignments in the encoding by grouping them into a coarser grid structure, thereby reducing the number of clauses needed to forbid forbidden combinations.

If this is right

  • Chen's product encoding is no longer optimal for AtMostOne.
  • The new monotone circuit for threshold-2 improves the best known size after fifty years.
  • Encodings of AtMost_k now scale linearly with n for k up to roughly the cube root of n.
  • Any encoding of AtMostOne must contain at least roughly √n auxiliary clauses.
  • The first unconditional nontrivial lower bound for this constraint is now known.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar compression ideas could be applied to Exactly-k or AtLeast-k constraints to obtain comparable savings.
  • The reduced clause counts may translate directly into faster SAT solving times for optimization problems that encode cardinality bounds.
  • The circuit improvement suggests that other threshold functions may admit smaller monotone circuits than previously known.
  • The grid-compression method might generalize to non-cardinality constraints that involve forbidding certain Hamming-weight patterns.

Load-bearing premise

The algebraic constructions and grid-compression steps produce correct, valid CNF formulas for every sufficiently large n without hidden polynomial factors that would erase the asymptotic savings.

What would settle it

An exhaustive enumeration for n around 100 that either shows the minimal clause count exceeds the stated upper bound or exhibits a concrete assignment that satisfies the proposed clauses yet violates the AtMostOne constraint.

Figures

Figures reproduced from arXiv: 2603.28954 by Andrew Krapivin, Benjamin Przybocki, Bernardo Subercaseaux.

Figure 1
Figure 1. Figure 1: Illustration of our proposed change of perspective on Chen’s product encoding [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Illustration of the multipartite encoding. Parts violating the [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Example for the disjunctive switching technique. True input variables are highlighted in [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Example of the generalized product encoding for [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Illustration of the grid compression framework [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Comparison of encodings for AtMost2 (UNSAT). We abbreviate the generalized product encoding as GP and its disjunctive variant as DGP. smallest propagation-complete encoding of an antitone 2-CNF function is always 2-CNF. While an affirmative answer has some prima facie plausibility, our construction concretely demonstrates how wide clauses can be useful even for AtMostOne, the simplest antitone 2-CNF functi… view at source ↗
read the original 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 $\text{AtMostOne}(x_1,\dots,x_n)$ constraint using $2n + 2 \sqrt{2n} + O(\sqrt[3]{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 + \sqrt{n+1} - 2$ clauses, which is the first nontrivial unconditional lower bound for this constraint and answers a question of Ku\v{c}era, Savick\'y, and Vorel. We then turn our attention to encodings of $\text{AtMost}_k(x_1,\dots,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(\sqrt[3]{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 \le 5$ and $7n - o(n)$ for $k \ge 6$.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript presents novel CNF encodings for cardinality constraints. It gives an explicit construction for the AtMostOne(x1,…,xn) constraint using 2n + 2√(2n) + O(n^{1/3}) clauses, refuting the conjectured optimality of Chen's product encoding. It also provides a lower bound of 2n + √(n+1) - 2 clauses. For AtMost_k, it introduces grid compression to achieve 2n + o(n) clauses when k = o(n^{1/3}) and 4n + o(n) when k = o(n). The work additionally improves the monotone circuit size for the threshold-2 function, improving on Adleman's 50-year-old construction.

Significance. If the constructions hold, this is a significant contribution: it supplies the first nontrivial unconditional lower bound for AtMostOne encodings (answering Kučera et al.), refutes a long-standing conjecture on optimal clause counts, and solves an open problem in monotone circuit complexity. The grid compression technique is presented as a general, hash-table-inspired method that yields asymptotically improved encodings for a range of k, with potential impact on both theory and practical SAT encodings.

minor comments (3)
  1. [Abstract] Abstract: standardize the big-O notation from O(∛n) to O(n^{1/3}) for consistency with standard mathematical writing.
  2. [Lower bound section] The lower-bound argument (information-theoretic or counting) would benefit from an explicit statement of the counting measure used to obtain the √(n+1) term.
  3. [Construction section] Include a small concrete example (e.g., n=9 or n=16) illustrating how grid compression produces the auxiliary variables and clauses for AtMostOne.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our manuscript and for recommending minor revision. The report does not list any specific major comments requiring point-by-point response. We appreciate the recognition of the significance of our results, including the new AtMostOne encoding, the matching lower bound, the grid compression technique, and the improvement to monotone circuit complexity for threshold-2. We will make any minor adjustments as needed in the revised version.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's central results consist of explicit constructive CNF encodings for AtMostOne and AtMost_k constraints, together with an information-theoretic lower bound. The upper-bound construction relies on grid compression and auxiliary variables to achieve the stated clause counts; the lower bound follows from a direct counting argument on the number of clauses needed to forbid certain assignments. Neither step reduces to a fitted parameter, self-definition, or load-bearing self-citation; both are presented as self-contained combinatorial arguments independent of prior fitted values or author-specific uniqueness theorems.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard mathematical axioms for counting and asymptotic analysis; no free parameters are fitted to data and no new entities are postulated.

axioms (1)
  • standard math Standard properties of asymptotic notation, square roots, and clause counting in CNF formulas.
    Invoked when deriving the O(n^{1/3}) term and the √n lower bound.

pith-pipeline@v0.9.0 · 5592 in / 1267 out tokens · 42420 ms · 2026-05-14T00:30:06.222093+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [1]

    Aaronson

    S. Aaronson. P ?=N P . In J. F. Nash, Jr. and M. T. Rassias, editors,Open Problems in Mathemat- ics, pages 1–122. Springer International Publishing, 2016.doi:10.1007/978-3-319-32162-2_1 . 8

    work page doi:10.1007/978-3-319-32162-2_1 2016

  2. [2]

    Ajtai, J

    M. Ajtai, J. Koml´ os, and E. Szemer´ edi. Sorting in clogn parallel steps.Combinatorica, 3(1):1–19, 1983.doi:10.1007/BF02579338. 3

    work page doi:10.1007/bf02579338 1983

  3. [3]

    Amano and A

    K. Amano and A. Maruoka. The monotone circuit complexity of quadratic boolean functions. Algorithmica, 46(1):3–14, 2006.doi:10.1007/s00453-006-0073-0. 2, 8

    work page doi:10.1007/s00453-006-0073-0 2006

  4. [4]

    As´ ın, R

    R. As´ ın, R. Nieuwenhuis, A. Oliveras, and E. Rodr´ ıguez-Carbonell. Cardinality net- works: a theoretical and empirical study.Constraints, 16(2):195–221, 2011. doi:10.1007/ S10601-010-9105-0. 1, 3

    work page 2011

  5. [5]

    Bailleux and Y

    O. Bailleux and Y. Boufkhad. Efficient CNF encoding of boolean cardinality constraints. In F. Rossi, editor,Principles and Practice of Constraint Programming - CP, volume 2833 ofLecture Notes in Computer Science, pages 108–122. Springer, 2003.doi:10.1007/978-3-540-45193-8\ _8. 1

    work page doi:10.1007/978-3-540-45193-8 2003

  6. [6]

    Ben-Haim, A

    Y. Ben-Haim, A. Ivrii, O. Margalit, and A. Matsliah. Perfect hashing and CNF encodings of cardinality constraints. In A. Cimatti and R. Sebastiani, editors,Theory and Applications of Satisfiability Testing - SAT, volume 7317 ofLecture Notes in Computer Science, pages 397–409. Springer, 2012.doi:10.1007/978-3-642-31612-8\_30. 1, 2

    work page doi:10.1007/978-3-642-31612-8 2012

  7. [7]

    Biere, T

    A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, and F. Pollitt. CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT Competition 2024. In M. Heule, M. Iser, M. J¨ arvisalo, and M. Suda, editors,Proc. of SAT Competition 2024 – Solver, Benchmark and Proof Checker Descriptions, volume B-2024-1 ofDepartment of Computer Science Report Series B, pages...

    work page 2024

  8. [8]

    P. M. Bittner, T. Th¨ um, and I. Schaefer. SAT encodings of the at-most-k constraint. In P. C. ¨Olveczky and G. Sala¨ un, editors,Software Engineering and Formal Methods, pages 127–144. Springer International Publishing, 2019. 31

    work page 2019

  9. [9]

    P. A. Bloniarz.The complexity of monotone boolean functions and an algorithm for finding shortest paths on a graph. PhD thesis, Massachusetts Institute of Technology, 1979. 2, 7, 8, 14 16

    work page 1979

  10. [10]

    J. A. Bondy. Induced subsets.J. Combinatorial Theory Ser. B, 12:201–202, 1972. doi: 10.1016/0095-8956(72)90025-1. 24

    work page doi:10.1016/0095-8956(72)90025-1 1972

  11. [11]

    S. Bublitz. Decomposition of graphs and monotone formula size of homogeneous functions. Acta Inform., 23(6):689–696, 1986.doi:10.1007/BF00264314. 2, 8

    work page doi:10.1007/bf00264314 1986

  12. [12]

    J. Chen. A new SAT encoding of the at-most-one constraint. InProc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation, 2010. 1, 2, 7, 14

    work page 2010

  13. [13]

    T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein.Introduction to algorithms. MIT Press, Cambridge, MA, third edition, 2009. 3

    work page 2009

  14. [14]

    P. E. Dunne.Techniques for the analysis of monotone Boolean networks. PhD thesis, University of Warwick, 1984. 7, 19

    work page 1984

  15. [15]

    E´ en and N

    N. E´ en and N. S¨ orensson. Translating pseudo-boolean constraints into SAT.J. Satisf. Boolean Model. Comput., 2(1-4):1–26, 2006.doi:10.3233/SAT190014. 3

    work page doi:10.3233/sat190014 2006

  16. [16]

    Emdin, A

    G. Emdin, A. S. Kulikov, I. Mihajlin, and N. Slezkin. CNF encodings of symmetric functions. Theory Comput. Syst., 68(5):1291–1311, 2024.doi:10.1007/S00224-024-10168-W. 1, 8, 15

    work page doi:10.1007/s00224-024-10168-w 2024

  17. [17]

    Erd˝ os, P

    P. Erd˝ os, P. Frankl, and Z. F¨ uredi. Families of finite sets in which no set is covered by the union ofrothers.Israel J. Math., 51(1-2):79–89, 1985.doi:10.1007/BF02772959. 14

    work page doi:10.1007/bf02772959 1985

  18. [18]

    A. M. Frisch and P. A. Giannaros. SAT encodings of the at-most- k constraint: Some old, some new, some fast, some slow. InProc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation, 2010. 1, 3, 6, 8, 9, 10

    work page 2010

  19. [19]

    I. P. Gent. Arc consistency in SAT. In F. van Harmelen, editor,Proceedings of the 15th European Conference on Artificial Intelligence, ECAI’2002, Lyon, France, July 2002, pages 121–125. IOS Press, 2002. 2

    work page 2002

  20. [20]

    M. I. Grinchuk. On the monotone complexity of threshold functions.Metody Diskret. Anal., 52:41–48, 120, 1992. 7

    work page 1992

  21. [21]

    P. Hall. On representatives of subsets.J. London Math. Soc., 10(1):26–30, 1935. doi: 10.1112/jlms/s1-10.37.26. 26

    work page doi:10.1112/jlms/s1-10.37.26 1935

  22. [22]

    T. B. Idalino and L. Moura.A Survey of Cover-Free Families: Constructions, Appli- cations, and Generalizations, pages 195–239. Springer Nature Switzerland, 2023. doi: 10.1007/978-3-031-48679-1_11. 14

    work page doi:10.1007/978-3-031-48679-1_11 2023

  23. [23]

    PySAT: A Python toolkit for prototyping with SAT oracles

    A. Ignatiev, A. Morgado, and J. Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. InSAT, pages 428–437, 2018.doi:10.1007/978-3-319-94144-8_26. 15, 32

    work page doi:10.1007/978-3-319-94144-8_26 2018

  24. [24]

    S. Jukna. Disproving the single level conjecture.SIAM J. Comput., 36(1):83–98, 2006. doi:10.1137/S0097539705447001. 2, 8

    work page doi:10.1137/s0097539705447001 2006

  25. [25]

    Karpi´ nski

    M. Karpi´ nski. CNF encodings of cardinality constraints based on comparator networks, 2019. arXiv:1911.00586. 15

    work page arXiv 2019

  26. [26]

    Kautz and R

    W. Kautz and R. Singleton. Nonrandom binary superimposed codes.IEEE Transactions on Information Theory, 10(4):363–377, 1964.doi:10.1109/TIT.1964.1053689. 14 17

    work page doi:10.1109/tit.1964.1053689 1964

  27. [27]

    R. E. Krichevskii. Complexity of contact circuits realizing a function of logical algebra.Soviet Physics. Doklady, 8:770–772, 1964. 8

    work page 1964

  28. [28]

    Kuˇ cera, P

    P. Kuˇ cera, P. Savick´ y, and V. Vorel. A lower bound on CNF encodings of the at-most-one constraint.Theor. Comput. Sci., 762:51–73, 2019. doi:10.1016/J.TCS.2018.09.003. 1, 2, 4, 8, 14, 15, 20, 21, 22

    work page doi:10.1016/j.tcs.2018.09.003 2019

  29. [29]

    Lenz and I

    K. Lenz and I. Wegener. The conjunctive complexity of quadratic boolean functions.Theoret. Comput. Sci., 81(2):257–268, 1991.doi:10.1016/0304-3975(91)90194-7. 2, 8

    work page doi:10.1016/0304-3975(91)90194-7 1991

  30. [30]

    Marques-Silva and I

    J. Marques-Silva and I. Lynce. Towards robust CNF encodings of cardinality constraints. In C. Bessiere, editor,Principles and Practice of Constraint Programming - CP, volume 4741 ofLecture Notes in Computer Science, pages 483–497. Springer, 2007. doi:10.1007/ 978-3-540-74970-7\_35. 1

    work page 2007

  31. [31]

    Mirwald and C

    R. Mirwald and C. P. Schnorr. The multiplicative complexity of quadratic boolean forms. Theoret. Comput. Sci., 102(2):307–328, 1992.doi:10.1016/0304-3975(92)90235-8. 2, 8

    work page doi:10.1016/0304-3975(92)90235-8 1992

  32. [32]

    Nguyen, V

    V. Nguyen, V. Nguyen, K. Kim, and P. Barahona. Empirical study on SAT-encodings of the at-most-one constraint. InSMA 2020: The 9th International Conference on Smart Media and Applications, Jeju, Republic of Korea, September 17 - 19, 2020, pages 470–475. ACM, 2020. doi:10.1145/3426020.3426170. 1, 31

    work page doi:10.1145/3426020.3426170 2020

  33. [33]

    J. E. Reeves.Cardinality Constraints in Boolean Satisfiability Solving. PhD thesis, Carnegie Mellon University, 2025. 1

    work page 2025

  34. [34]

    I. S. Sergeev. On the complexity of monotone circuits for threshold symmetric boolean functions. Diskret. Mat., 32(1):81–109, 2020.doi:10.4213/dm1547. 7, 15, 19

    work page doi:10.4213/dm1547 2020

  35. [35]

    C. Sinz. Towards an optimal CNF encoding of boolean cardinality constraints. In P. van Beek, editor,Principles and Practice of Constraint Programming - CP, volume 3709 ofLecture Notes in Computer Science, pages 827–831. Springer, 2005. doi:10.1007/11564751\_73. 1, 2, 8, 12, 15, 24, 25

    work page doi:10.1007/11564751 2005

  36. [36]

    E. Sperner. Ein Satz ¨ uber Untermengen einer endlichen Menge.Math. Z., 27(1):544–548, 1928. doi:10.1007/BF01171114. 32

    work page doi:10.1007/bf01171114 1928

  37. [37]

    Wegener.The complexity of Boolean functions

    I. Wegener.The complexity of Boolean functions. John Wiley & Sons, Inc., 1987. 7, 19

    work page 1987

  38. [38]

    capacity

    E. Wynn. A comparison of encodings for cardinality constraints in a SAT solver, 2018. URL: https://arxiv.org/abs/1810.12975,arXiv:1810.12975. 31 A Proofs for Section 3.2 A.1 Proof of Lemma 1 Lemma 1.There is a propagation-complete encoding of the AtMostOne′(x1, . . . , xn; z)constraint using2n+O( √n)clauses andO( √n)auxiliary variables. 18 Proof. Rename t...

    work page arXiv 2018