TAOCP 7.2.2.2 Exercise 486
In the direct encoding, each variable $x_i$ is represented by Boolean variables indicating its possible values.
Section 7.2.2.2: Satisfiability
Exercise 486. [21] [21] (Late Binding solitaire.) Shuffle a deck and deal out 18 cards; then try to reduce these 18 piles to a single pile, using a sequence of "captures" in which one pile is placed on top of another pile. A pile can capture only the pile to its immediate left, or the pile found by skipping left over two other piles. Furthermore a capture is permitted only if the top card in the capturing pile has the same suit or the same rank as the top card in the captured pile. For example, consider the following deal:
$$J\heartsuit\ 5\diamondsuit\ 10\clubsuit\ 8\diamondsuit\ J\clubsuit\ A\spadesuit\ 4\clubsuit\ A\heartsuit\ 4\diamondsuit\ 4\clubsuit\ 5\diamondsuit\ 10\spadesuit\ A\clubsuit\ 6\heartsuit\ 10\diamondsuit\ 10\diamondsuit$$
Ten captures are initially possible, including $5\diamondsuit \times J\diamondsuit$, $A\spadesuit \times 10\spadesuit$, and $5\diamondsuit \times 5\clubsuit$. Some captures then make others possible, as in $8\spadesuit \times 8\clubsuit \times 8\diamondsuit$.
If captures must be made "greedily" from left to right as soon as possible, this game is the same as the first 18 steps of a classic one-player game called "Idle Year," and we wind up with five piles [see Dick's Games of Patience (1883), 50–52]. But if we cleverly hold back until all 18 cards have been dealt, we can do much better.
Show that one can win from this position, but not if the first move is $A\spadesuit \times J\clubsuit$.
Verified: no
Solve time: 3m45s
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. ∎