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)
$\begingroup$
$\endgroup$
2
-
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 DeckerCommented Sep 15, 2016 at 20:16
-
1$\begingroup$ @Rick : Yes, this's the basic implementation $\endgroup$– GilfoyleCommented Sep 16, 2016 at 9:31
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
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).
$\begingroup$
$\endgroup$
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.
