TAOCP 7.2.2.2 Exercise 392

Section 7.2.2.2: Satisfiability

Exercise 392. [22] [22] The blank spaces in the following diagrams can be filled with letters in such a way that all occurrences of the same letter are rookwise connected:

a) Demonstrate how to do it. (Puzzle $(i)$ is easy; the others less so.) b) Similarly, solve the following puzzles, but use kingwise connectedness instead.

c) Construct clauses with which a SAT solver can solve general puzzles of this kind: Given a graph $G$ and disjoint sets of vertices $T_1, T_2, \ldots, T_t$, a solution should exhibit disjoint connected sets of vertices $S_1, S_2, \ldots, S_t$ with $T_j \subseteq S_j$ for $1 \le j \le t$.

Verified: no
Solve time: 3m56s

---

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