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čera, Savický, 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$.

翻译：我们提出了若干新颖的基数约束编码方法，其使用的子句数量少于现有基准，更重要的是，引入了构建紧凑编码的全新通用技术。首先，针对$\text{AtMostOne}(x_1,\dots,x_n)$约束，我们给出一个CNF编码，仅需使用$2n + 2 \sqrt{2n} + O(\sqrt[3]{n})$个子句，从而反驳了Chen乘积编码的猜想最优性。该构造还生成了更小规模的阈值-2函数单调电路，改进了Adleman五十年前的构造，并偶然解决了电路复杂性中一个长期悬而未决的问题。另一方面，我们证明任何对此约束的编码至少需要$2n + \sqrt{n+1} - 2$个子句，这是该约束首个非平凡无条件下界，并回答了Kučera、Savický与Vorel提出的问题。随后，我们转向$\text{AtMost}_k(x_1,\dots,x_n)$的编码问题，引入受哈希表启发的“网格压缩”技术：当$k = o(\sqrt[3]{n})$时，编码仅需$2n + o(n)$个子句；当$k = o(n)$时，编码仅需$4n + o(n)$个子句。此前已知的最小编码规模为：当$k \le 5$时$(k+1)n + o(n)$个子句，当$k \ge 6$时$7n - o(n)$个子句。