TAOCP 7.2.2.2 Exercise 486
For part (a), take the ordered vertex set $(v_1,v_2,v_3,v_4)$ and let the edges be v_1v_2,\quad v_2v_3,\quad v_3v_1,\quad v_1v_4,\quad v_3v_4 .
Section 7.2.2.2: Satisfiability
Exercise 486. [21] [21] (Late Binding solitaire.) Shuffle a deck and deal out 18 cards; then try to reduce these 18 piles to a single pile, using a sequence of "captures" in which one pile is placed on top of another pile. A pile can capture only the pile to its immediate left, or the pile found by skipping left over two other piles. Furthermore a capture is permitted only if the top card in the capturing pile has the same suit or the same rank as the top card in the captured pile. For example, consider the following deal:
$$J\heartsuit\ 5\diamondsuit\ 10\clubsuit\ 8\diamondsuit\ J\clubsuit\ A\spadesuit\ 4\clubsuit\ A\heartsuit\ 4\diamondsuit\ 4\clubsuit\ 5\diamondsuit\ 10\spadesuit\ A\clubsuit\ 6\heartsuit\ 10\diamondsuit\ 10\diamondsuit$$
Ten captures are initially possible, including $5\diamondsuit \times J\diamondsuit$, $A\spadesuit \times 10\spadesuit$, and $5\diamondsuit \times 5\clubsuit$. Some captures then make others possible, as in $8\spadesuit \times 8\clubsuit \times 8\diamondsuit$.
If captures must be made "greedily" from left to right as soon as possible, this game is the same as the first 18 steps of a classic one-player game called "Idle Year," and we wind up with five piles [see Dick's Games of Patience (1883), 50–52]. But if we cleverly hold back until all 18 cards have been dealt, we can do much better.
Show that one can win from this position, but not if the first move is $A\spadesuit \times J\clubsuit$.
Verified: no
Solve time: 3m55s
Solution
For part (a), take the ordered vertex set $(v_1,v_2,v_3,v_4)$ and let the edges be
$$ v_1v_2,\quad v_2v_3,\quad v_3v_1,\quad v_1v_4,\quad v_3v_4 . $$
The vertices $v_1,v_2,v_3$ form a triangle, so the graph is not $2$-colorable. It is not the complete graph $K_4$, because $v_2v_4$ is missing, and the coloring
$$ v_1=1,\qquad v_2=2,\qquad v_3=3,\qquad v_4=2 $$
uses three colors. Hence the chromatic number is exactly $3$.
This graph is quenchable. The edge $v_1v_4$ permits a move of type (iii) with $l=1$. The resulting graph has vertex set $(v_3,v_4)$, and these two vertices are adjacent because of the edge $v_3v_4$. A type (ii) move with $k=1$ deletes $v_3$, leaving the single vertex $v_4$. Therefore the graph satisfies the recursive definition of quenchability.
For part (b), let
$$ x_{t,i,j}=[v_i\to v_j\text{ at time }t] $$
denote that the two surviving vertices in positions $i$ and $j$ are adjacent after $t$ quenching moves. At time $0$, the clauses fix the original graph:
$$ x_{0,i,j} $$
for every edge $v_iv_j$, and
$$ \bar{x}_{0,i,j} $$
for every nonedge $v_iv_j$.
For each time $t$, exactly one quenching move must be selected. The possible type (ii) moves are represented by variables $q_{t,k}$, where choosing $q_{t,k}$ deletes vertex $k$ and requires the edge between positions $k$ and $k+1$. The possible type (iii) moves are represented by variables $s_{t,l}$, where choosing $s_{t,l}$ deletes positions $l$ and $l+1$ and requires the edge between positions $l$ and $l+3$.
The choice clauses are
$$ \bigvee_k q_{t,k}\vee\bigvee_l s_{t,l} $$
together with the pairwise exclusion clauses
$$ \bar q_{t,k}\vee\bar q_{t,k'} $$
for distinct $k,k'$, the clauses
$$ \bar s_{t,l}\vee\bar s_{t,l'} $$
for distinct $l,l'$, and
$$ \bar q_{t,k}\vee\bar s_{t,l} $$
for all $k,l$. Thus at most one move is chosen, and the first clause forces at least one move whenever more than one vertex remains.
The legality of a type (ii) move is expressed by
$$ \bar q_{t,k}\vee x_{t,k,k+1}. $$
The legality of a type (iii) move is expressed by
$$ \bar s_{t,l}\vee x_{t,l,l+3}. $$
The transition clauses describe the new adjacency relation. Suppose $q_{t,k}$ is selected. Every vertex with position greater than $k$ shifts down by one position, while the vertices before $k$ keep their positions. Hence for all surviving pairs $(i,j)$ at time $t+1$ the clauses
$$ \bar q_{t,k}\vee\bar x_{t,i',j'}\vee x_{t+1,i,j} $$
and
$$ \bar q_{t,k}\vee x_{t,i',j'}\vee\bar x_{t+1,i,j} $$
are included, where $(i',j')$ is the pair of old positions corresponding to the new pair $(i,j)$ after deleting position $k$.
For a type (iii) move selected by $s_{t,l}$, positions after $l+1$ shift down by two, and the transition clauses are
$$ \bar s_{t,l}\vee\bar x_{t,i',j'}\vee x_{t+1,i,j} $$
and
$$ \bar s_{t,l}\vee x_{t,i',j'}\vee\bar x_{t+1,i,j}, $$
where $(i',j')$ is obtained from $(i,j)$ by reversing this shift after deletion of positions $l$ and $l+1$.
Finally, the terminal condition requires that the remaining graph has one vertex. The variables $q_{t,k}$ and $s_{t,l}$ are only needed while at least two vertices remain, so after $n-1$ possible reductions the surviving state must have size one. The clauses above form a finite Boolean formula whose satisfying assignments correspond exactly to legal quenching sequences.
If the graph is quenchable, choose the variables $q_{t,k}$ and $s_{t,l}$ according to a valid sequence of quenching moves and set the $x$ variables according to the resulting graphs at each time. Every clause is then satisfied. Conversely, a satisfying assignment chooses one legal move at every nonterminal time, because the choice and legality clauses enforce this property, and the transition clauses force the $x$ variables to describe the graphs obtained from those moves. The terminal clauses force the process to end with one vertex. Therefore the graph is quenchable.
This completes the proof. ∎