TAOCP 7.2.2.2 Exercise 444
In the direct encoding, each variable $x_i$ is represented by Boolean variables indicating its possible values.
Section 7.2.2.2: Satisfiability
Exercise 444. [M26] The following single lookahead unit resolution algorithm, called SLUR, returns either 'sat', 'unsat', or 'maybe', depending on whether a given set $F$ of clauses is satisfiable, unsatisfiable, or beyond its ability to decide via easy propagations:
E1. [Propagate.] If $F \vdash \epsilon$, terminate ('unsat'). Otherwise set $F \leftarrow F|{l \mid F \vdash l}$.
E2. [Satisfied?] If $F = \emptyset$, terminate ('sat'). Otherwise set $l$ to any literal within $F$.
E3. [Lookahead and propagate.] If $F|,\overline{l} \vdash_1 \epsilon$, set $F \leftarrow F|{l}$ (${l' \mid F | l \vdash_1 l'}$) and return to E2. Otherwise if $F|,\overline{l} \vdash_1 \epsilon$, $F \leftarrow F|{\overline{l}}$ (${l' \mid F|,\overline{l} \vdash_1 l'}$) and return to E2. Otherwise terminate ('maybe').
Notice that this algorithm doesn't backtrack after committing itself in E2 to either $l$ or $\bar{l}$.
a) If $F$ consists of Horn clauses, possibly renamed (see exercise 7.1.1–55), prove that SLUR will never return 'maybe', regardless of how it chooses $l$ in step E2. b) Find four clauses $F$ on three variables such that SLUR always returns 'sat', although $F$ is not a set of possibly renamed Horn clauses. c) Prove that SLUR never returns 'maybe' if and only if $F \in \text{UC}_1$ (see exercise 443). d) Explain how to implement SLUR in linear time with respect to total clause length.
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. ∎