Notes on SAT Encodings of Cardinality Constraints

atleast_k(x₁, …, x_n) is true iff at least k of the n arguments are true.

The challenge is to give

a small explicit formula
actually, a DAG, that means, we can re-use subformulas
equivalently, a formula in conjunctive normal form (we can Tseitin-transform the DAG)

We should distinguish

the asserting variant: a CNF that asserts that the constraint is true
the computing variant: a CNF that asserts that the value of the constraint is equal to an extra variable (if we Tseitin-transform, then this is the variable that corresponds to the root node of the DAG)

References

some basics (in German) http://www.imn.htwk-leipzig.de/~waldmann/edu/ws16/cp/folien/#(67)
some references are in in this thread https://github.com/Z3Prover/z3/issues/755

Applications

An Old Idea (for Atmost-One)

Recall the product encoding for atmost-one (Chen, 2010; cited in (Hölldobler and Nguyen, 2013). It is based on the following observation:

We arrange the inputs in a rectangular matrix (any shape will do), and consider the projections (the disjunction) of elements in each column, and of elements in each row. Then, atmost-one of the inputs is true exactly iff atmost-one of the column projections is true and atmost-one of the row projections is true.

This allows for a recursive construction. E.g., arrange inputs in a square matrix, then Atmost-one for size n recurs to two Atmonst-one of size sqrt(n) (and if size is small enough, we bail out and use a simple direct encoding)

Mathematically, we were using this theorem:

For large enough n, the set S = {1, …, n} has two partitions P₁, P₂ such that for any two distinct elements of S, there is at least one of these partitions that has these elements in different classes.

Can we make this work for Atmost-k?

Definition: A partition P of M separates a set S ⊆ M if each element of S is in a distinct P-class.

Example: [[0, 1, 8], [2, 3, 4], [5, 6, 7]] separates {1, 2, 5}, but not {1, 2, 3}.

Definition: A collection of partitions {P₁, …, P_p} of M is called k-separating if each k-element subset S ⊆ M is separated by at least one of the P_i.

Example:

[[0,1,2],[3,4,5],[6,7,8]]
[[0,3,6],[1,4,7],[2,5,8]]

is 2-separating. (This models the atmost-1-implementation mentioned above.)

Example:

[[0,1,8],[2,3,4],[5,6,7]]
[[0,2,6],[1,4,5],[3,7,8]]
[[0,3,5],[1,2,7],[4,6,8]]
[[0,4,7],[1,3,6],[2,5,8]]

is 3-separating. (with a permutation of letters, you can think of the rows, the colums, and the parallels to the two diagonals in a 3 by 3 matrix)

Example:

[[0,1],[2,3],[4,7],[5,6]]
[[0,2],[1,7],[3,5],[4,6]]
[[0,3],[1,4],[2,5],[6,7]]
[[0,4],[1,3],[2,6],[5,7]]
[[0,5],[1,6],[2,7],[3,4]]
[[0,7],[1,2],[3,6],[4,5]]

is 4-separating. This can be used to make an encoding for “atleast 4 of 8” with 40 variables and 111 clauses. That is smaller than the direct encoding (a clause for each 4-subset) which takes 80 variables and 432 clauses. (Both numbers measured with ersatz which may introduce extra variables because of sloppy implementation of Tseitin transformation.)

Observations on 2-separation

In all the data below, k = separation, n = number of elements, p = number of partitions, c = k

Binary encoding of atmost-1 (atleast-2) is from this 2-separating partition:

k = 2 n = 8 p = 3 c = 2
[[0,1,2,3],[4,5,6,7]]
[[0,2,4,6],[1,3,5,7]]
[[0,1,4,5],[2,3,6,7]]

and this can be extend. Partition P_i is obtained by looking at binary digit at position i.

Observations on 3-separation

3-separating collections of partitions of n elements

n = 6 with 3 partitions

[[0,2],[1,3],[4,5]]
[[0,3],[1,5],[2,4]]
[[0,5],[1,2],[3,4]]

n = 9 with 4, see above

n = 10 with 5

[[0,1,2,9],[3,5],[4,6,7,8]]
[[0,2,5,8],[1,3,4,7],[6,9]]
[[0,3,6,7],[1,8],[2,4,5,9]]
[[0,4],[1,5,6,7],[2,3,8,9]]
[[0,5,6,8],[1,3,4,9],[2,7]]

n = 12 with 6

[[0,1,2,3,6],[4,7,8,9,10],[5,11]]
[[0,1,2,3,11],[4,5,7,10],[6,8,9]]
[[0,1,5,6,7],[2,8,10,11],[3,4,9]]
[[0,4,5,6,7,9],[1,11],[2,3,8,10]]
[[0,4,8],[1,3,5,6,10],[2,7,9,11]]
[[0,9,10,11],[1,3,7,8],[2,4,5,6]]

n = 14 with 7

[[0,1,2,13],[3,7,9,10,11],[4,5,6,8,12]]
[[0,1,3,6,11,12,13],[2,5,7,9],[4,8,10]]
[[0,2,3,4,6,9,10],[1,5,8],[7,11,12,13]]
[[0,3,5,11],[1,8,9,12,13],[2,4,6,7,10]]
[[0,4,7,12],[1,6,10,11,13],[2,3,5,8,9]]
[[0,5,7,8,11,12],[1,3,4],[2,6,9,10,13]]
[[0,6,9],[1,5,7,10,13],[2,3,4,8,11,12]]

n = 20 with 10

[[0,1,3,6,7,13,15],[2,4,10,14,16,19],[5,8,9,11,12,17,18]]
[[0,1,11,12,14,15],[2,3,4,6,7,9,18],[5,8,10,13,16,17,19]]
[[0,2,3,8,14,17],[1,6,9,10,13,15,19],[4,5,7,11,12,16,18]]
[[0,2,13,16,18],[1,4,5,9,12,15],[3,6,7,8,10,11,14,17,19]]
[[0,3,4,11,12,13,14,17],[1,2,7,8,9,15,16,19],[5,6,10,18]]
[[0,3,5,7,8,10,12,16,19],[1,2,6,17,18],[4,9,11,13,14,15]]
[[0,3,9,12,15,16],[1,5,7,8,19],[2,4,6,10,11,13,14,17,18]]
[[0,4,6,8,12,16],[2,7,9,11,13],[3,5,10,14,15,17,18,19]]
[[0,5,6,12,13,15,17],[1,4,9,14,18,19],[2,3,7,8,10,11,16]]
[[0,9,10,14,17],[1,2,4,5,6,7,8,13,18],[3,11,12,15,16,19]]

(there is on element missing in one of the partitions, that means it does not matter in which class it goes, separation will be achieved in any case)

This suggests that we can find, for each n, a 3-separating collection of n/2 partitions. Can you prove this?