30 July 2014

At Most R

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 1s to the right. Once I see a group of more than $6$ I say BAD!. But how exactly do we push 1s 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 1s are dropped from the first row. These 1s are dropped only if they would come adjacent to the 1s that were dropped earlier. I omit some of these steps when they are not interesting. For example, if no 1s are dropped, then I omit the dropping step.

Hongseok Yang described this process as ‘moving a basked underneath the original values, and collecting the 1s’. 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$ 1s, 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$.

mikolas said...

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.