TAOCP 7.2.2.2 Exercise 399
In the direct encoding, each variable $x_i$ is represented by Boolean variables indicating its possible values.
Section 7.2.2.2: Satisfiability
Exercise 399. [23] [23] If the variables $u$ and $v$ range over $d$ values ${1, \ldots, d}$, it's natural to encode them directly as sequences $u_1 \ldots u_d$ and $v_1 \ldots v_d$, where $u_i = [u = i]$ and $v_j = [v = j]$, using the at-least-one clauses and the at-most-one clauses (17). A binary constraint tells us which pairs $(i, j)$ are legal; for example, the graph-coloring constraint says that $i \ne j$ when $i$ and $j$ are the colors of adjacent vertices in some graph.
One way to specify such a constraint is to assert the preclusion clauses $(\bar{u}_i \vee \bar{v}_j)$ for all illegal pairs $(i, j)$, as we did for graph coloring in (16). But there's also another general way: We can assert the support clauses
$$\bigwedge_{i=1}^{d} \Bigl(\bar{u}i \vee \bigvee{v_j \mid (i,j) \text{ is legal}}\Bigr) ;\wedge; \bigwedge{j=1}^{d} \Bigl(\bar{v}_j \vee \bigvee{u_i \mid (i,j) \text{ is legal}}\Bigr)$$
instead. Graph coloring with $d$ colors would then be clauses such as $(u_3 \vee v_1 \vee v_2 \vee v_4 \vee \cdots \vee v_d)$, when $u$ and $v$ are adjacent.
a) Suppose $f$ of the $d^2$ pairs $(i, j)$ are legal. How many preclusion clauses are needed? How many support clauses? b) Prove that the support clauses are always at least as strong as the preclusion clauses, in the sense that all consequences of the preclusion clauses under unit propagation are also consequences of the support clauses under unit propagation, given any assignment consistent with the binary variables $(u_1, \ldots, u_d, v_1, \ldots, v_d)$. c) Conversely, in the case of the graph-coloring constraint, the preclusion clauses are also at least as strong as the support clauses (hence equally strong). d) However, exhibit a binary constraint for which the support clauses are strictly stronger than the preclusion clauses.
Verified: no
Solve time: 4m06s
Solution
In the direct encoding, each variable $x_i$ is represented by Boolean variables indicating its possible values. Write
$$ x_{i,j}=1\iff x_i=j, $$
where $0\le i<p$ and $1\le j\le d$ if the domain has size $d$. The direct encoding already contains the clauses forcing each $x_i$ to have exactly one value. The all-different constraint adds the requirement that two different variables cannot choose the same value.
For two distinct variables $x_i$ and $x_k$, and for any value $j$, the assignment
$$ x_{i,j}=x_{k,j}=1 $$
must be forbidden. The corresponding clause is
$$ \bar{x}{i,j}\vee \bar{x}{k,j}. $$
Taking all pairs of variables and all possible values gives the complete encoding:
$$ \bigwedge_{0\le i<k<p}\ \bigwedge_{1\le j\le d} (\bar{x}{i,j}\vee\bar{x}{k,j}). $$
These clauses are sufficient. Suppose the direct variables represent an assignment satisfying the clauses. If two variables $x_i$ and $x_k$ had the same value $j$, then the direct encoding would require
$$ x_{i,j}=1,\qquad x_{k,j}=1. $$
The clause
$$ \bar{x}{i,j}\vee\bar{x}{k,j} $$
would then be false, contradicting satisfiability. Hence no two variables receive the same value.
They are also necessary. Given any assignment satisfying the all-different constraint, no pair of variables $x_i,x_k$ has the same value. Therefore, for every $j$, at least one of $x_{i,j}$ and $x_{k,j}$ is false, so every clause
$$ \bar{x}{i,j}\vee\bar{x}{k,j} $$
is satisfied.
Thus the all-different constraint in the direct encoding is enforced by adding one binary clause for every pair of variables and every possible value:
$$ \boxed{\bar{x}{i,j}\vee\bar{x}{k,j}\qquad (0\le i<k<p,\ 1\le j\le d).} $$
This completes the proof. ∎