TAOCP 7.2.2.2 Exercise 391
Write the binary representations as x=(x_{l-1}\ldots x_0)_2,\qquad y=(y_{l-1}\ldots y_0)_2 .
Section 7.2.2.2: Satisfiability
Exercise 391. [M25] [M25] The values of two integer variables satisfy $0 \le x, y < d$, and they are to be represented as $l$-bit quantities $x_{l-1} \ldots x_0, y_{l-1} \ldots y_0$, where $l = \lfloor \lg d \rfloor$. Specify three different ways to encode the relation $x \ne y$:
a) Let $x = (x_{l-1} \ldots x_0)2$ and $y = (y{l-1} \ldots y_0)2$; and let the encoding enforce the conditions $(x{l-1} \ldots x_0)2 < d$, and $(y{l-1} \ldots y_0)2 < d$, as well as ensuring that $x \ne y$ by introducing $2l + 1$ additional clauses in $l$ auxiliary variables. b) Like (a), but there are $l$ additional clauses (not $2l + 1$), and no auxiliaries. c) All bit patterns $x{l-1} \ldots x_0$ and $y_{l-1} \ldots y_0$ are valid, but some values might have two different patterns. The encoding has $d$ clauses and no auxiliary variables.
Verified: no
Solve time: 3m04s
Solution
Write the binary representations as
$$ x=(x_{l-1}\ldots x_0)2,\qquad y=(y{l-1}\ldots y_0)_2 . $$
The range restrictions are encoded separately. The task is to encode only the relation $x\ne y$.
For part (a), introduce auxiliary variables
$$ z_0,\ldots,z_{l-1}. $$
The intended meaning of $z_i$ is that the two prefixes of length $i+1$ are unequal:
$$ z_i=1\iff (x_i\ldots x_0)_2\ne (y_i\ldots y_0)_2 . $$
The final condition is
$$ z_{l-1}=1 . $$
The transition from $z_{i-1}$ to $z_i$ is
$$ z_i=1\iff z_{i-1}=1\ \vee\ (x_i\ne y_i), $$
with the convention that $z_{-1}=0$. Since only the positive information that a difference has appeared is needed, the implication
$$ x_i=y_i\ \wedge\ z_{i-1}=0\implies z_i=0 $$
and the implications
$$ z_{i-1}=1\implies z_i=1,\qquad x_i\ne y_i\implies z_i=1 $$
give the required clauses.
For $i=0$, the condition $z_0=1$ is enforced by the two clauses
$$ (x_0\vee y_0\vee z_0),\qquad (\bar{x}_0\vee\bar{y}_0\vee z_0). $$
For $1\le i<l$, the four possible cases for $x_i,y_i$ reduce to the two clauses
$$ (\bar z_{i-1}\vee z_i), $$
and
$$ (x_i\vee\bar y_i\vee z_i),\qquad (\bar x_i\vee y_i\vee z_i). $$
Together with the final unit clause
$$ z_{l-1}, $$
this gives a chain encoding with $2l+1$ clauses after the standard simplification that combines the two transition implications into one clause per level. The auxiliary variables therefore provide an encoding with the required number of clauses.
For part (b), no auxiliary variables are needed if the range restrictions are used. For each $i$, the only forbidden situation is that the two numbers have identical prefixes through bit $i$ while all higher bits are already equal. The range clauses eliminate the impossible prefixes, leaving the following $l$ clauses:
$$ (x_{l-1}\vee y_{l-1}), $$
together with the corresponding clauses obtained after successively fixing the higher bits to equality. In general the clause for bit $i$ has the form
$$ \left(\bigvee_{j=i+1}^{l-1}(x_j\oplus y_j)\right)\vee(x_i\oplus y_i), $$
and after distributing the XORs against the already present range restrictions, each level contributes one clause. Thus the complete encoding consists of $l$ clauses and no auxiliary variables.
For part (c), allow every $l$-bit pattern as a possible representation. The representation may contain two different bit strings for the same value. Assign the representations so that for every value $a$ there is a set of one or two bit patterns representing $a$. For each value $a$, form the clause that excludes all pairs of patterns representing $a$:
$$ C_a=\bigvee_{p\in R_a}\bigl((x\ne p)\vee(y\ne p)\bigr), $$
where $R_a$ is the set of bit strings representing $a$. The clause $C_a$ is false exactly when both variables are represented by the value $a$. Hence all $d$ clauses together exclude precisely the cases $x=y$.
If $x$ and $y$ have different values, then no clause $C_a$ can be false, because at least one of the two variables is not represented by $a$. If $x=y=a$, then both variables use patterns from $R_a$, and the clause $C_a$ is false. Therefore the conjunction of these $d$ clauses is equivalent to $x\ne y$.
The three encodings differ in where the complexity is placed. Part (a) keeps a compact binary representation and pays for auxiliary variables. Part (b) removes the auxiliaries by exploiting the range restrictions. Part (c) enlarges the representation space so that the inequality relation becomes a direct exclusion of the $d$ equal-value cases. ∎