How do I use canonical ordering to reduce symmetry in the SAT encoding of the pigeonhole problem?

Question

In the paper "Efficient CNF Encoding for Selecting 1 from N Objects", the authors introduce their "commander variable" technique for encoding the constraint, and then talk about the pigeonhole problem.

Since my error may exist in lower-level understanding, let me declare what I think I know before posing the question:

Let $m$ and $n$ be the number of pigeons and holes. The naive encoding uses a propositional variable $X_{i,j}$ that is true when the $i'th$ pigeon is to be put in the $j'th$ hole. The clause $ExactlyOne(X_{1,1}, X_{1,2}, ..., X_{1,n})$ enforces that pigeon 1 must occupy exactly one hole; identical clauses are added for the other pigeons. The clause $AtMostOne(X_{1,1}, X_{2,1}, ..., X_{m,1})$ enforces that no more than one pigeon occupies hole 1; identical clauses are added for the remaining holes.

When there are more pigeons than holes (m > n), the problem is unsolvable (obvious to humans) but the SAT solver doesn't "see" this fact. When it can't find a way to place pigeons $1,2,3,..,m$ it will search an attempt with pigeons $2,1,3,...,m$. It doesn't understand that the order of the pigeons is irrelevant. The paper, among others, calls this symmetry.

Instances where $m=n+1$ are used as a strenuous test of a SAT solver's ability to detect unsatisfiability.

The paper proposes to break the symmetry by enforcing order on pigeons. Pigeon $i$ must be placed in a hole in front of the hole of pigeon $i+1$ (i.e., the pigeon in hole $j$ must have a smaller number than of the pigeon in hole $j+1$). It then disappointingly says, "Due to space limitations, we do not explicitly describe in detail the canonical-ordering encoding, but the number of clauses generated is of order $O(n*log(n))$".

So my question is: what did they do to get these results?

I want to treat the variables $\{X_{1,1}, X_{2,1}, ..., X_{m,1}\}$ as string of bits that, numerically, identifies the choice of which pigeon went into hole 1, and so on. Follow this with $n-1$ comparators to enforce the paper's suggestion. My naive comparator construction, however, requires m clauses, one for each bit (of increasingly ugly size). Help! :)

Answer 1

Let $m$ be the number of pigeons and $n$ be the number of holes. Let the propositional variables $B_{i,0}$ ... $B_{i,log(n)}$ encode the binary representation of $j-1$ if the $i$th pigeon is put into the $j$th hole. (Example, if pigeon 1 were placed in hole 10, $j - 1 = 9$, which is binary 1001. So $B_{1,3}$ = true, $B_{1,2}$ = false, $B_{1,1}$ = false and $B_{1,0}$ = true.)

Enforce a particular ordering of the pigeons in the holes by requiring that the hole encoded by the $B_{i}$ variables is less than that of $B_{i+1}$. The encodings are compared as you would expect:

$B_{i,log(n)}$ < $B_{i+1,log(n)}$
OR
$B_{i,log(n)}$ = $B_{i+1,log(n)}$ AND $B_{i,log(n)-1}$ < $B_{i+1,log(n)-1}$
OR
$B_{i,log(n)}$ = $B_{i+1,log(n)}$ AND $B_{i,log(n)-1}$ = $B_{i+1,log(n)-1}$ AND $B_{i,log(n)-2}$ < $B_{i+1,log(n)-2}$
OR
...

... following the pattern of allowing the most significant bits to be equivalent as long as the next bit to the right is less than that of the next pigeon. There will be $O(log(n))$ conjunctions per comparator and $O(m)$ comparators, giving the expected $O(m * log(n))$ additional clauses.

The $B$ variable values must be implied by the $X_{i,j}$ values. Each $B_{i,*}$ bit is implied by any one of a particular set of the $X_{i,j}$ variables being set. Example: assuming $n = 16$, you would have:

$ExactlyOne(X_{1,9}, X_{1,10}, X_{1,11}, X_{1,12}, X_{1,13}, X_{1,14}, X_{1,15}, X_{1,16}, \overline{B_{1,3}})$

which forces $B_{1,3}$ true if pigeon 1 is placed in any of holes 9-16. Otherwise $B_{1,3}$ is set false to satisfy the clause. These clauses set the remaining $B_{i}$ bits.

$ExactlyOne(X_{1,5}, X_{1,6}, X_{1,7}, X_{1,8}, X_{1,13}, X_{1,14}, X_{1,15}, X_{1,16}, \overline{B_{1,2}})$ $ExactlyOne(X_{1,3}, X_{1,4}, X_{1,7}, X_{1,8}, X_{1,11}, X_{1,12}, X_{1,15}, X_{1,16}, \overline{B_{1,1}})$ $ExactlyOne(X_{1,2}, X_{1,4}, X_{1,6}, X_{1,8}, X_{1,10}, X_{1,12}, X_{1,14}, X_{1,16}, \overline{B_{1,0}})$

There will be $log(n)$ of these clauses for each pigeon. Since there are $m$ pigeons, $m * log(n)$ clauses are added.