TAOCP 7.2.2.2 Exercise 469

Let the squares of the $m \times n$ board have coordinates $(i,j)$, with $1 \le i \le m$ and $1 \le j \le n$.

taocpmathematicsalgorithmsvolume-4

Section 7.2.2.2: Satisfiability

Exercise 469. ▶ [**] [$M25$] Find a certificate of unsatisfiability $(C_1, C_2, \ldots, C_t)$ for the fact that an $8 \times 8$ chessboard minus cells $(1, 8)$ and $(8, 1)$ cannot be exactly covered by dominoes $h_{ij}$ and $v_{ij}$ that are fixed under all of the even-odd endomorphisms. Each $C_k$ for $1 \le k \le t$ should be a single positive literal. (Therefore the clauses for this problem belong to the relatively simple class $\text{PC}_2$ in the hierarchy of exercise 443.)

Verified: no
Solve time: 5m53s

Solution

Let the squares of the $m \times n$ board have coordinates $(i,j)$, with $1 \le i \le m$ and $1 \le j \le n$. The endomorphism in the even-odd rule (190) chooses, for each square, one of its two possible domino directions according to the parity of its coordinates. A fixed point is therefore a domino covering in which every square is paired in the direction prescribed by (190).

Assume first that $m$ is even. In this case the rule pairs the squares in each column by vertical dominoes. Indeed, for each column $j$, the square pairs in the order

$$ (1,j)\leftrightarrow(2,j),\quad (3,j)\leftrightarrow(4,j),\quad \dots,\quad (m-1,j)\leftrightarrow(m,j). $$

These pairs cover every square of the column because $m$ is even. Hence the collection of these vertical dominoes is a domino covering, and every domino is unchanged by (190), so this covering is a fixed point.

To prove uniqueness, consider any fixed point. The top square $(1,j)$ of each column has only the partner prescribed by (190), namely $(2,j)$. Therefore every fixed point must contain the domino

$$ {(1,j),(2,j)}. $$

Removing these dominoes leaves the same problem on rows $3$ through $m$. Repeating this argument forces the dominoes

$$ {(3,j),(4,j)},\ldots,{(m-1,j),(m,j)} $$

for every column $j$. Thus no other covering can be fixed.

Now assume that $m$ is odd. Since $mn$ is even, $n$ must be even. The same argument with the roles of rows and columns interchanged applies. The rule forces horizontal dominoes in each row:

$$ ( i,1)\leftrightarrow(i,2),\quad ( i,3)\leftrightarrow(i,4),\quad \dots,\quad (i,n-1)\leftrightarrow(i,n). $$

These dominoes form a covering because $n$ is even. Every fixed point must contain the domino covering the leftmost square $(i,1)$ of each row, then the domino covering $(i,3)$, and so on. Hence this horizontal covering is forced and unique.

In both possible cases, one of $m,n$ is even because $mn$ is even. The even dimension determines a covering fixed by the even-odd rule, and the forced domino containing the first square in each corresponding strip shows that no second fixed point can exist.

This completes the proof.

∎