Near-Optimal Encodings of Cardinality Constraints

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č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$.

Figures (6)

• Figure 1: Illustration of our proposed change of perspective on Chen's product encoding
• Figure 2: Illustration of the multipartite encoding. Parts violating the $\mathsf{AtMostOne}$-vertex constraint are shaded red. Parts for which $z_k$ is true are shaded teal.
• Figure 3: Example for the disjunctive switching technique. True input variables are highlighted in green. The ✓ and ✗ symbols indicate whether the encoding should be satisfiable for the given $d$.
• Figure 4: Example of the generalized product encoding for $k=2$
• Figure 5: Illustration of the grid compression framework

Theorems & Definitions (66)

• Theorem 1: Multipartite Encoding
• Theorem 2
• Theorem 3: Grid Compression
• Theorem 4: Disjunctive Grid Compression
• Definition 1: CNF Encoding
• Definition 2: Propagation Completeness lower-bound
• Lemma 1
• proof : Proof sketch
• proof : Proof of \ref{['thm:am1']}
• Theorem 5: Clique Encoding