Near-Optimal Encodings of Cardinality Constraints

TL;DR

This paper introduces new, more efficient CNF encodings for cardinality constraints, improving clause counts and providing new techniques with theoretical and practical implications in circuit complexity.

Contribution

It presents the first nontrivial lower bounds for AtMostOne encodings and introduces grid compression, a novel technique for more compact encodings.

Findings

A CNF encoding for AtMostOne with 2n + 2√(2n) + O(∛n) clauses.

A smaller monotone circuit for the threshold-2 function, solving a long-standing open problem.

New bounds for AtMost_k encodings using grid compression, reducing clause counts.

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