Requiring at least one alldiff constraint to be satisfied converted to SAT

Question

For generating certain hard puzzles, I am trying to model a problem (ultimately) in SAT. I don't know how to do that, so I am starting with CSP because it's more expressive. In CSP, there is a global alldiff constraint, which requires all variables to take on different values from their domains. I have a set of alldiff constraints. However, out of this set, I only require at least one of them to be true. That is, not all of them have to be satisfied.

For concreteness, suppose we have 8 variables $x_1,\ldots,x_8$. Each take values from the domain $\{0,1,2\}$. We want to satisfy the following formula:

$$\text{alldiff}(x_1,x_2,x_3) \lor \text{alldiff}(x_1,x_6,x_7) \lor \text{alldiff}(x_4,x_5,x_6) \lor \text{alldiff}(x_3,x_4,x_8).$$

We are happy if at least one of the 4 alldiff clauses is satisfied, e.g., if $x_1=0$, $x_2=1$, and $x_3=2$, we are already happy.

But how is then modeled in SAT? Specifically, how do we write an alldiff constraint in SAT?

Answer 1

If you want to model an alldiff() constraint in SAT, there are several options. Here are two different options you can try:

• One way is to expand $\text{alldiff}(x_1,\dots,x_n)$ into $n(n-1)/2$ inequality constraints: $(x_1 \ne x_2) \land (x_1 \ne x_3) \land \cdots$. Now you can express each inequality constraint $x_i \ne x_j$ on $b$-bit values in turn as a boolean formula: $(x_i[0] \ne x_j[0]) \lor (x_i[1] \ne x_j[1]) \lor \cdots$, where $x_i[k]$ is the $k$th bit of $x_i$. In this way each alldiff constraint on $n$ $b$-bit variables expands into a boolean formula of size $\Theta(n^2 b)$.

• Alternatively, a different way is to use a one-hot encoding. Suppose each $x_i$ needs to take values from some universe $U$ of $u$ values. Instead of encoding each $x_i$ as a $\lceil \lg u \rceil$-bit value, encode it as a $u$-bit boolean vector, where $x_i[k]=1$ if $x_i = k$ and $x_i[k]=0$ otherwise. Now an alldiff constraint on $n$ variables amounts to requiring that there are exactly $n$ ones in the $nu$-bit vector obtained by concatenating the vectors for each of the $n$ variables in the alldiff constraint. Thus, we obtain a $n$-out-of-$nu$ constraint.

  This $n$-out-of-$nu$ constraint can be encoded in multiple ways; one way is to use a tree of half-adders to sum up these values. The tree will have $nu$ leaves, and with a $\lceil \lg nu \rceil$-bit output at the root. You can find more about encoding cardinality constraints here: https://cs.stackexchange.com/a/6522/755.

These approaches give you a boolean formula, i.e., a boolean circuit; it's not in CNF form. So, strictly speaking, it's not an instance of SAT. However, there is a standard way to convert any such boolean formula to CNF form: you use the Tseitin transform (equivalently, you use the standard reduction from CircuitSAT to SAT) and then run a SAT solver on the result. There are several SAT front-ends that will do this work for you; STP is one I have used that is quite convenient, but there are others as well.

This gives you at least options you could consider, for converting your problem to SAT. Which one is most efficient might depend on your specific problem and the parameters of your problem (the size of the domain, the number of variables in each alldiff constraint).

Also, if you have a lot of alldiff constraints, it seems likely that a CSP solver might do better than a SAT solver. CSP solvers are designed to handle alldiff constraints well, thus they might perform better than naively bitblasting to SAT, as SAT solvers won't be aware of that structure.

See also When to use SAT vs Constraint Satisfaction? and Converting (math) problems to SAT instances and https://cs.stackexchange.com/a/12153/755.