6
$\begingroup$

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)

$\endgroup$
  • 1
    $\begingroup$ By "better" do you mean something shorter than (for $n=3, k=4$) $(x_1\ge 1)\land(x_1\le 4) \land(x_2\ge 1)\land(x_2\le 4)\land(x_3\ge 1)\land(x_3\le 4)\land(x_1\ne x_2)\land(x_1\ne x_3)\land(x_2\ne x_3)$ $\endgroup$ – Rick Decker Sep 15 '16 at 20:16
  • 1
    $\begingroup$ @Rick : Yes, this's the basic implementation $\endgroup$ – Gilfoyle Sep 16 '16 at 9:31
1
$\begingroup$

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

$\endgroup$
0
$\begingroup$

This is sometimes known as an "alldiff" constraint. There are some encodings listed here: Requiring at least one alldiff constraint to be satisfied converted to SAT.

Alternatively, you might do better to use a CSP solver, rather than trying to express this in CNF and then use a SAT solver. Handling "alldiff" constraints is exactly the sort of thing that constraint satisfaction solvers are designed to do well. See When to use SAT vs Constraint Satisfaction?.

Also relevant: Encoding 1-out-of-n constraint for SAT solvers, Reduce the following problem to SAT.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.