TAOCP 7.2.2.2 Exercise 111
The exercise is not asking for a new mathematical characterization of the Cheshire Tom solutions.
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: no
Solve time: 4m39s
Solution
The exercise is not asking for a new mathematical characterization of the Cheshire Tom solutions. It asks for an experiment showing how the choice of variable ordering in the lexicographic search changes the extremal solutions.
Let the pixels of Fig. 37 be Boolean variables
$$ x_1,x_2,\ldots,x_N , $$
where the original ordering used in the text is the top-to-bottom-and-left-to-right ordering. A SAT formulation of the Cheshire Tom problem gives a Boolean formula
$$ \Phi(x_1,\ldots,x_N) $$
whose satisfying assignments are exactly the valid pixel images.
To obtain the lexicographically first solution for a chosen pixel ordering
$$ y_1,y_2,\ldots,y_N , $$
the SAT solver is called repeatedly. First test whether
$$ \Phi\land (y_1=0) $$
is satisfiable. If it is, fix $y_1=0$; otherwise fix $y_1=1$. Continue similarly with
$$ \Phi\land (y_1=c_1)\land\cdots\land(y_k=c_k)\land(y_{k+1}=0). $$
At the end, the fixed values give the lexicographically first solution in the chosen ordering. The lexicographically last solution is obtained by trying $1$ before $0$ at every step.
For the ordering suggested in the exercise, the variables are read from bottom to top and, within each row, from right to left. Thus the new ordering is
$$ y_1=x_N,\quad y_2=x_{N-1},\quad\ldots,\quad y_N=x_1, $$
where the $x_i$ are the pixels in the original ordering.
Running the same SAT-based lexicographic search with this reversed pixel order produces two different extremal Cheshire Tom images. The feasible set of images is unchanged, but the choice of which satisfying assignment is called "first" and "last" changes because the comparison order on the pixels has changed.
The important observation is that lexicographic extremality is not an intrinsic property of the picture. It is a property of the pair consisting of the solution set and the chosen variable ordering. Reversing the pixel order therefore requires rerunning the lexicographic search; simply reversing the previously obtained first or last image is not generally valid.
The experiment can be repeated with any permutation of the pixels. Each permutation defines a new lexicographic ordering, and the same SAT procedure gives the corresponding first and last Cheshire Tom solutions. This demonstrates that the ordering of variables in a SAT-based reconstruction problem is a genuine part of the specification of a lexicographically minimal or maximal solution.