*How to encode a cardinality constraint as boolean constraints.*

**Motivation.**
All problems in NP can be encoded as a SAT problem, because SAT is NP-complete.
Often you need to say that $x_1+\cdots+x_n \le r$.
For example, you might want to do this to reduce MAXSAT to SAT.
(And we know that MAXSAT is useful for static analysis.)
MAXSAT is an optimization problem; SAT is its decision version.
The general strategy to reduce optimization to decision is to use binary search.
So that's what we'll do.

The input of MAXSAT is a set $\{C_1,\ldots,C_n\}$ of clauses. The question is what is the maximum number of clauses that can be satisfied. To solve this, we ask several SAT questions of the following form: $$\begin{align} (C_1 \lor y_1) \land (C_2 \lor y_2) \land\ldots\land (C_n \lor y_n) \land {\it encode}(y_1+\cdots+y_n \le r) \end{align}$$

If $r=0$, then all the auxiliary variables $y_1,\ldots,y_n$ must be $0$. In this case, the question asks if all clauses can be satisfied. On the other hand, if $r=n$, then the answer is yes, by setting $y_1=\cdots=y_n=1$. In general, the question asks the following: ‘Is it possible to satisfy $n-r$ clauses (simultaneously)?’

**How to Do It.**
I knew for some time that efficient encodings exist, but I didn't look them up.
At some point I needed the case $r=1$, and I was able to find a good solution.
Now that I read how the general $r$ works I think the encoding is kinda cute.
The encoding was found by Carsten Sinz in 2005.

Here's an example for $r=6$:

10100001011010110111 1100001011010110111 110001011010110111 11001011010110111 1101011010110111 111011010110111 11111010110111 1111110110111 111111110111

What's happening here?
I'm pushing the `1`s to the right.
Once I see a group of more than $6$ I say BAD!.
But how exactly do we push `1`s with a boolean circuit?
And how many auxiliary variables do we need?
Clearly, the gray ones are just the original values.
But what's the general rule to compute the others?

Here's the same computation, but more explicit this time.

10100001011010110111 0000000 1000000 drop 1000000 shift 1100000 drop 1100000 shift 1100000 shift 1100000 shift 1100000 shift 1110000 drop 1110000 shift 1111100 drop 1111100 shift 1111110 drop 1111110 shift 1111111 drop

This time the original variables are in the first line, and all the others are auxiliaries.
There are two kinds of steps that alternate.
First, there are steps in which the group of $r+1$ auxiliaries are shifted to the right.
Second, there are steps where a group of consecutive `1`s are dropped from the first row.
These `1`s are dropped only if they would come adjacent to the `1`s that were dropped earlier.
I omit some of these steps when they are not interesting.
For example, if no `1`s are dropped, then I omit the dropping step.

Hongseok Yang described this process as ‘moving a basked underneath the original values, and collecting the `1`s’.
I think that's a pretty good image to have in mind.

It should now be clear how this is done with a boolean circuit. Dropping is done with AND-gates, between the auxiliary from the left and the original from above. Next, any boolean circuit can be transformed into a conjunctive normal form, using the Tseitin transformation.

**Details.**
If the original variables are $x_1,\ldots,x_n$, then we introduce auxiliaries $y_i^j$ for $1 \le i \le r+1$ and $0 \le j$ and $i+j \le n$.
The clauses are
$$\begin{align}
y_i^{j-1} &\to y_i^j &&\text{for shifting} \\
y_{i-1}^j \land x_{i+j} &\to y_i^j &&\text{for dropping} \\
y_1^j\land y_2^j \land\ldots\land y_{r+1}^j &\to 0 && \text{for detecting bad situations}
\end{align}$$

Yes, I am being sloppy with some boundary situations. Also, I'm using slightly more variables than necessary: Can you see how batches of $r$ auxiliaries (rather than batches of $r+1$ auxiliaries) are enough?

**Others.**
There's also an encoding based on dividing the array of booleans in half.
You compute for each half if you have *at least* $k$ `1`s, for $1 \le k \le r+1$.
You then aggregate the results for halves into the result for the whole array.

Using either of these methods you can encode equality constraints, like $x_1+\cdots+x_n=r$.

## 2 comments:

Also an important property of cardinality encoding is arc consistency, i.e. that if a value is semantically enforced under an assignment, it is also enforced by unit propagation. For instance, one could try to build a binary tree of binary counters but this is unlikely to be AC.

Thanks: I didn't know of arc consistency.

1. By important, you mean important for efficiency, right?

2. I think you can make an adder "arc consistent", but you need (too?) many clauses. For example, to compute C = A xor B, you can say (¬a and ¬b → ¬c) and (¬a and b → c) and (a and ¬b → c) and (a and b → ¬c).

## Post a Comment

Note: (1) You need to have third-party cookies enabled in order to comment on Blogger. (2) Better to copy your comment before hitting publish/preview. Blogger sometimes eats comments on the first try, but the second works. Crazy Blogger.