TAOCP 7.2.2.2 Exercise 407

Number the rows and columns of the diagram from $0$ to $3$.

taocpmathematicsalgorithmsvolume-4math-medium

Section 7.2.2.2: Satisfiability

Exercise 407. [M22] [M22] If $x$, $y$, $z$ are order-encoded, with $0 \le x, y < d$ and $0 \le z < 2d-1$, the clauses

$$\bigwedge_{k=1}^{2d-2} \bigwedge_{j=\max(0,k+1-d)}^{k} (x^j \vee \bar{y}^{k-j} \vee z^k)$$

are satisfiable if and only if $x + y \le z$; this is the basic idea underlying (20). Another way to encode the same relation is to introduce new order-encoded variables $u$ and $v$, and to construct clauses for the relations $\lfloor x/2 \rfloor + \lfloor y/2 \rfloor \le u$ and $\lceil x/2 \rceil + \lceil y/2 \rceil \le v$, recursively using methods for numbers less than $\lfloor d/2 \rfloor$ and $\lceil d/2 \rceil + 1$. Then we can finish the job by letting $z^1 = v^1$, $z^{2d-2} = v^0$ ($d$ even) or $u^{d-1}$ ($d$ odd), and appending the clauses

$$(\bar{u}^j \vee z^{2j}) \wedge (\bar{v}^{j+1} \vee z^{2j}) \wedge (\bar{u}^j \vee \bar{v}^{j+1} \vee z^{2j+1}), \quad \text{for } 1 \le j \le d-2.$$

  • a) Explain why this alternative method is valid.
  • b) For what values of $d$ does that method produce fewer clauses?
  • c) Consider analogous methods for the relation $x + y \ge z$.

Verified: no
Solve time: 3m46s

Solution

Number the rows and columns of the diagram from $0$ to $3$. A rearrangement that works is

$$ \begin{array}{|c|c|c|c|} \hline T&H&E&A\ \hline T&R&O&F\ \hline U&C&M&G\ \hline P&M&I&N\ \hline \end{array} $$

The phrase to be traced, ignoring the separators, is

$$ \text{THEARTOFCOMPUTERPROGRAMMING}. $$

A sequence of positions that traces this phrase is

$$ \begin{aligned} &(0,0),(0,1),(0,2),(0,3),(1,1),(0,0),(1,2),(1,3),(2,1),\ &(1,2),(2,2),(3,0),(2,0),(1,0),(0,2),(1,1),(3,0),\ &(1,1),(1,2),(2,3),(1,1),(0,3),(2,2),(3,1),(3,2),\ &(3,3),(2,3). \end{aligned} $$

Reading the letters in these positions gives

$$ \begin{aligned} &T,H,E,A,R,T,O,F,C,O,M,P,U,T,E,R\ &\qquad P,R,O,G,R,A,M,M,I,N,G, \end{aligned} $$

which is exactly

$$ \text{THE_ART_OF_COMPUTER_PROGRAMMING}. $$

For consecutive positions in the displayed path, the displacement is always either a king move, meaning that the row and column changes are each at most $1$, or a knight move, meaning that the absolute changes are $1$ and $2$ in some order. The only repeated type of move that needs checking is the transition between the final occurrences of letters, and the last transition is

$$ (3,3)\rightarrow(2,3), $$

which is a king move. Thus the former exceptional step from $R$ to $G$ has also been replaced by a legal move.

Therefore the rearranged diagram above permits the complete phrase to be traced using only king moves and knight moves.

$$ \boxed{ \begin{array}{|c|c|c|c|} \hline T&H&E&A\ \hline T&R&O&F\ \hline U&C&M&G\ \hline P&M&I&N\ \hline \end{array} } $$

This completes the solution. ∎