比如我们此前的八皇后问题:
range R = 1..8;
var{int} x[R] in R;
solve {
forall (i in R, j in R: i < j) {
x[i] \\neq x[j];
x[i] \\neq x[j] - (j-i);
x[i] \\neq x[j] + (j-i);
}
}
我们可以直接写成:
solve {
AllDifferent(x)
AllDifferent(x[i] + i for i in R)
AllDifferent(x[i] - i for i in R)
}
如果存在任意一个子集 $S \subseteq X$ 使得
$$ \left| \bigcup_{x_i \in S} D(x_i) \right| < |S| $$
则此时必然无法找到令 $S$ 中变量取各不同值的解,整个也就无解。
反之,如果对任意的子集 $S$,都有 $\left| \bigcup_{x_i \in S} D(x_i) \right| \ge |S|$,那么则存在一个将这些变量各自分配到不同值的可行解。