CNF form of variable assignment problem

There are n variables $x_1$, $x_2$,..., $x_n$ and each one of them takes values from 1 to k (k>= n) and all are distinct. How can I represent this in the CNF form? (I tried the trivial way of trying all assignments and then checking if they are distinct, but I think it could be done better)

If you only have to encode this (and don't have any other constraints on $x_i$), you can then use the following constraints:
$x_1 < x_2 < \dots < x_{n-1} < x_n \leq k$
which is $n$ constraints.

Let $m=\lceil \log_2 k\rceil$ and $x_i = b_{im}, b_{i(m-1)}, \dots, b_{i1}$, where $m$ is the high bit and $1$ is the low bit.
Define $d_{ij} = b_{ij}\textrm{ XOR }b_{(i+1)j}$.
Then, the constraint $x_1 < x_2$ is representable as:
$$
\bigvee_{i=1}^{m} \left[\left(\bigwedge_{j=i+1}^m d_{1j}'\right)\left(b_{2i}b_{1i}'\right)\right] = 1
$$
basically the i-th clause encodes that the top $m-i$ bits are identical and the $i$-th bit is $1$ in $x_2$ and $0$ in $x_1$.

Abusing notation slightly (taking the constants in the representation of $k$ for $x_{n+1}$), a similar technique can be used for $x_n \leq k$, where one would add an extra clause $\bigwedge_i d_{ni}'$ for handling the equality.

The above formula is a DNF. To get to CNF, one would simple encode $\textrm{NOT}(x_2 \leq x_1)$.

Finally, if it's needed to represent $x_1 \geq 1$ one can do this by adding a CNF clause $\bigvee_i b_{1i}$.

Note that the complexity here is really good. $O(nm)$ clauses, and $O(nm^2)$ literals. In particular if $n$ and $k$ are large this is much better than for other techniques (but it isn't applicable in other settings where other constraints could change the ordering).

StackExchange Computer Science Q#63505, answer score: 2