TAOCP 7.2.2.2 Exercise 442
In the direct encoding, each variable $x_i$ is represented by Boolean variables indicating its possible values.
Section 7.2.2.2: Satisfiability
Exercise 442. ▶ [M27] [M27] The unit propagation relation $\vdash_1$ can be generalized to $k$th order propagation $\vdash_k$ as follows: Let $F$ be a family of clauses and let $l$ be a literal. If $(l_1, l_2, \ldots, l_p)$ is a sequence of literals, we write $L_g^- = {l_1, \ldots, l_{g-1}, \bar{l}_g}$ for $1 \le g \le p$. Then
$$F \vdash_0 l \iff l \in F;$$
$$F \vdash_{k+1} l \iff F \mid L_g^- \vdash_k \epsilon, \text{ for } k \ge 0;$$
$$F \vdash_k e \iff F \vdash_k l \text{ for some distinct literals } l_1, l_2, \ldots, l_p \text{ with } l_p = l;$$
$$F \vdash_k e \iff F \vdash_k l \text{ for some literal } l.$$
a) Verify that $\vdash_1$ corresponds to unit propagation according to this definition. b) Describe $\vdash_2$ informally, using the concept of "failed literals." c) Prove that $F \vdash_k$ or $F \vdash_k l$ implies $F \mid l \vdash_k \epsilon$ for all literals $l$, and furthermore that $F \vdash_k \epsilon$ implies $F \vdash_{k+1} \epsilon$, for all $k \ge 0$. d) True or false: $F \vdash_k l$ implies $F \vdash_{k+1} l$. e) Let $L_k(F) = (F \mid \vdash_k l)$. What is $L_k(R')$, where $R'$ appears in (7) and $k \ge 0$? f) Given $k \ge 1$, explain how to compute $L_k(F)$ and $F \mid L_k(F)$ in $O(n^{2k-1}m)$ steps, when $F$ has $m$ clauses in $n$ variables.
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. ∎