TAOCP 7.2.2.2 Exercise 461

Exercise 461. [20] $[20]$ What additional clauses will rule out non-fixed points of $\tau_1$ and $\tau_2$?

Verified: no
Solve time: 5m13s

Solution

Let $X=(x_{ij})$ be an $m\times n$ binary matrix. The transformations $\tau_1$ and $\tau_2$ are endomorphisms for the sweep problem, so adding clauses that force $X$ to be fixed by them preserves the existence of satisfying assignments. The required clauses must exclude exactly those matrices that are changed by either transformation.

A matrix is fixed by $\tau_1$ precisely when each row is nondecreasing, and it is fixed by $\tau_2$ precisely when each column is nondecreasing. Therefore the forbidden local patterns are a $1$ followed immediately by a $0$ in a row, and a $1$ followed immediately by a $0$ in a column.

For adjacent entries in a row, the forbidden assignment is

$$ x_{ij}=1,\qquad x_{i,j+1}=0 . $$

The corresponding clause is

$$ \bar{x}{ij}\vee x{i,j+1}. $$

Adding these clauses for every $i$ and every $j$ with $1\le i\le m$ and $1\le j<n$ forces every row to satisfy

$$ x_{i1}\le x_{i2}\le \cdots \le x_{in}. $$

For adjacent entries in a column, the forbidden assignment is

$$ x_{ij}=1,\qquad x_{i+1,j}=0 . $$

The corresponding clause is

$$ \bar{x}{ij}\vee x{i+1,j}. $$

Adding these clauses for every $j$ and every $i$ with $1\le j\le n$ and $1\le i<m$ forces every column to satisfy

$$ x_{1j}\le x_{2j}\le \cdots \le x_{mj}. $$

Hence the additional clauses are

$$ {\bar{x}{ij}\vee x{i,j+1}:1\le i\le m,\ 1\le j<n} $$

together with

$$ {\bar{x}{ij}\vee x{i+1,j}:1\le i<m,\ 1\le j\le n}. $$

Every matrix satisfying these clauses has no decreasing adjacent pair in any row or column, so $\tau_1$ and $\tau_2$ cannot change it. Conversely, if a matrix is not fixed by $\tau_1$ or $\tau_2$, then it contains one of the two forbidden adjacent patterns above, and the corresponding clause is false. Thus these clauses rule out exactly the non-fixed points of $\tau_1$ and $\tau_2$.

This completes the proof. ∎