TAOCP 7.2.2.2 Exercise 407
In the direct encoding, each variable $x_i$ is represented by Boolean variables indicating its possible values.
Section 7.2.2.2: Satisfiability
Exercise 407. [M22] [M22] If $x$, $y$, $z$ are order-encoded, with $0 \le x, y < d$ and $0 \le z < 2d-1$, the clauses
$$\bigwedge_{k=1}^{2d-2} \bigwedge_{j=\max(0,k+1-d)}^{k} (x^j \vee \bar{y}^{k-j} \vee z^k)$$
are satisfiable if and only if $x + y \le z$; this is the basic idea underlying (20). Another way to encode the same relation is to introduce new order-encoded variables $u$ and $v$, and to construct clauses for the relations $\lfloor x/2 \rfloor + \lfloor y/2 \rfloor \le u$ and $\lceil x/2 \rceil + \lceil y/2 \rceil \le v$, recursively using methods for numbers less than $\lfloor d/2 \rfloor$ and $\lceil d/2 \rceil + 1$. Then we can finish the job by letting $z^1 = v^1$, $z^{2d-2} = v^0$ ($d$ even) or $u^{d-1}$ ($d$ odd), and appending the clauses
$$(\bar{u}^j \vee z^{2j}) \wedge (\bar{v}^{j+1} \vee z^{2j}) \wedge (\bar{u}^j \vee \bar{v}^{j+1} \vee z^{2j+1}), \quad \text{for } 1 \le j \le d-2.$$
- a) Explain why this alternative method is valid.
- b) For what values of $d$ does that method produce fewer clauses?
- c) Consider analogous methods for the relation $x + y \ge z$.
Verified: no
Solve time: 3m55s
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. ∎