TAOCP 7.2.2.2 Exercise 434
In the direct encoding, each variable $x_i$ is represented by Boolean variables indicating its possible values.
Section 7.2.2.2: Satisfiability
Exercise 434. [21] Let $L_l$ be the language defined by the regular expression $0^10^$; in other words, the binary string $x_1 \ldots x_n$ is in $L_l$ if and only if it consists of zero or more 0s followed by exactly 1 1s followed by zero or more 0s.
a) Explain why the following clauses are satisfiable if and only if $x_1, \ldots, x_n \in L_l$: (i) $(\bar{p}_0 \vee \bar{x}0)$, $(\bar{p}0 \vee p{k-1})$ for $1 \le k \le n$, also $(\bar{p}{k-1} \vee \bar{x}_k \vee \bar{p}_k)$ ... [text truncated at page boundary]
$(q_k \vee q_{k+1})$, and $(\bar{q}{k+1} \vee x_k \vee q_k)$ for $1 \le k \le n$, also $(q{n+1})$; (iii) $(\bar{r}k \vee p{k-1}) \wedge \bigwedge_{0 \le d \le l} (\bar{r}k \vee x{k+d}) \wedge (\bar{r}k \vee \bar{r}{k+1})$ for $1 \le k \le n+1-l$, also $(r_1 \vee \cdots \vee r_{n+1-l})$.
b) Show that those clauses are forcing when $l = 1$ but not when $l = 2$.
Verified: no
Solve time: 3m44s
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. ∎