TAOCP 7.2.2.2 Exercise 485

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 .

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 485. ▶ [23] [23] Sometimes successive transitions in the previous exercise are commutative: For example, the effect of $q_{t,k}$ and $q_{t,k+1}$ is the same as $q_{t,k+2}$ and $q_{t+1,k}$. Explain how to break symmetry in such cases, by allowing only one of the two possibilities.

Verified: no
Solve time: 3m50s

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. ∎