TAOCP 7.2.2.2 Exercise 409

In the direct encoding, each variable $x_i$ is represented by Boolean variables indicating its possible values.

Section 7.2.2.2: Satisfiability

Exercise 409. ▶ [M26] [M26] Continuing exercise 408, find the best makespans in the following cases:

a) $m = 3$; $n = 3t + 1$; $w_{1j} = w_{2(j+1)} = w_{3(j+s)} = a_j$ for $1 \le j \le r$; $w_{1n} = w_{2n} = w_{3n} = \lfloor (a_1 + \cdots + a_r)/2 \rfloor$; otherwise $w_{ij} = 0$. (The positive integers $a_j$ are given.)

b) $m = 4$; $n = r + 2$; $w_{1j} = (r+1)a_j$ and $w_{2j} = 1$ for $1 \le j \le r$; $w_{2(r+1)} = w_{2r} = (r+1)\lfloor (a_1 + \cdots + a_r)/2 \rfloor$; $w_{4n} = w_{4n} = w_{4r} = r - 1$; otherwise $w_{ij} = 0$.

c) $m = n$; $w_{jj} = n - 2$; $w_{jn} = w_{nj} = 1$ for $1 \le j < n$; otherwise $w_{ij} = 0$.

d) $m = 2$; $w_{1j} = a_j$ and $w_{2j} = b_j$ for $1 \le j \le n$, where $a_1 + \cdots + a_n = b_1 + \cdots + b_n = s$ and $a_j + b_j \le s$ for all $j$.

Verified: no
Solve time: 3m56s


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. ∎