How do I use canonical ordering to reduce symmetry in the SAT encoding of the pigeonhole problem?
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)}$ &lt; $B_{i+1,log(n)}$
OR
$B_{i,log(n)}$ = $B_{i+1,log(n)}$ AND $B_{i,log(n)-1}$ &lt; $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}$ &lt; $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.