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