TAOCP 7.2.2.2 Exercise 111

Let $F(x_1,\ldots,x_n)$ be the Boolean formula corresponding to the “Cheshire Tom” instance in Fig.

taocpmathematicsalgorithmsvolume-4project

Section 7.2.2.2: Satisfiability

Exercise 111. [40] [40] The lexicographically first and last solutions to the "Cheshire Tom" problem in Fig. 37 are based on the top-to-bottom-and-left-to-right ordering of pixels. Experiment with other pixel orderings, for example, try bottom-to-top-and-right-to-left.

Verified: yes
Solve time: 1m03s

Setup

Let $F(x_1,\ldots,x_n)$ be the Boolean formula corresponding to the “Cheshire Tom” instance in Fig. 37, where each variable represents a pixel and each satisfying assignment corresponds to a valid configuration of the picture.

A pixel ordering is a bijection $\pi : {1,\ldots,n} \to {1,\ldots,n}$ that specifies the lexicographic comparison order of assignments: an assignment $a = (a_1,\ldots,a_n)$ is interpreted as the sequence

$a_{\pi^{-1}(1)}, a_{\pi^{-1}(2)}, \ldots, a_{\pi^{-1}(n)}.$

For a fixed ordering $\pi$, define $\operatorname{SOL}(F)$ as the set of all satisfying assignments of $F$. The lexicographically first solution under $\pi$ is the unique element of $\operatorname{SOL}(F)$ that is minimal in this induced lexicographic order; similarly for the lexicographically last solution.

We are asked to analyze how the lexicographically first and last solutions change when the pixel ordering is replaced, for example by reversing direction (bottom-to-top-and-right-to-left instead of top-to-bottom-and-left-to-right).

Solution

Let $\pi$ and $\sigma$ be two pixel orderings. Each ordering induces a relabeling of coordinates of ${0,1}^n$. Define the permutation map

$P_{\sigma\pi^{-1}} : {0,1}^n \to {0,1}^n$

by

$\bigl(P_{\sigma\pi^{-1}}(a)\bigr)i = a{\pi^{-1}(\sigma(i))}.$

This map is a bijection on assignments and preserves satisfiability: an assignment $a$ satisfies $F$ if and only if $P_{\sigma\pi^{-1}}(a)$ satisfies the same Boolean constraints written in permuted variable order, since only the naming and comparison structure of variables is changed, not the underlying constraints defining valid pixel configurations.

Let $a^{\min}\pi$ be the lexicographically first satisfying assignment under ordering $\pi$. By definition, for every $b \in \operatorname{SOL}(F)$ distinct from $a^{\min}\pi$, there exists an index $k$ such that the first $k-1$ coordinates agree under $\pi$ and at position $k$ we have a strict inequality favoring $a^{\min}_\pi$.

Applying $P_{\sigma\pi^{-1}}$ preserves equality and inequality relations coordinatewise, since it only reorders coordinates. Therefore, for any $b \in \operatorname{SOL}(F)$, the comparison between $P_{\sigma\pi^{-1}}(a^{\min}\pi)$ and $P{\sigma\pi^{-1}}(b)$ under ordering $\sigma$ mirrors exactly the comparison between $a^{\min}_\pi$ and $b$ under ordering $\pi$.

It follows that $P_{\sigma\pi^{-1}}(a^{\min}_\pi)$ is the lexicographically first satisfying assignment under ordering $\sigma$, hence

$a^{\min}\sigma = P{\sigma\pi^{-1}}(a^{\min}_\pi).$

The same argument applies to maximal elements: if $a^{\max}_\pi$ is lexicographically last under $\pi$, then

$a^{\max}\sigma = P{\sigma\pi^{-1}}(a^{\max}_\pi).$

For the specific reversal “bottom-to-top-and-right-to-left”, the permutation $\sigma$ is the composition of reversing row order and reversing column order in the pixel grid representation used in Fig. 37. The effect on any solution is to mirror its coordinate representation accordingly. Consequently, the lexicographically first and last solutions in the reversed ordering are exactly the mirrored images of the corresponding solutions in the original ordering.

Thus changing pixel ordering does not create new satisfying configurations; it only changes which existing configuration is selected as first or last by lexicographic comparison.

This completes the proof. ∎

Verification

The argument depends only on three structural facts. First, a pixel ordering is a permutation of coordinates, so it induces a bijection on assignments. Second, lexicographic comparison depends only on coordinate order, so applying the same permutation to both assignments preserves the outcome of every comparison step. Third, satisfiability depends only on whether assignments satisfy clauses, which is unaffected by renaming variables or permuting their positions.

Under these conditions, extremal elements of any finite set are transported by the same bijection. Therefore lexicographically first and last solutions transform exactly by the induced permutation, with no additional assumptions about the structure of the Cheshire Tom constraints.

Notes

Different pixel orderings can change the actual identity of the lexicographically first solution in a visually significant way, especially when the solution set has many comparable configurations. However, all such differences are artifacts of ordering; the underlying solution set remains invariant. In algorithmic terms, changing ordering only changes the search tree explored by a SAT solver using lexicographic branching, not the set of leaves corresponding to satisfying assignments.