TAOCP 7.2.2.2 Exercise 484

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 484. [22] [22] (Graph quenching.) A graph with vertices $(v_1, \ldots, v_n)$ is called "quenchable" if either (i) $n = 1$; or (ii) there's a $k$ such that $v_k - v_{k+1}$ and the graph on $(v_1, \ldots, v_{k-1}, v_{k+1}, \ldots, v_n)$ can be quenched; or (iii) there's an $l$ such that $v_l - v_{l+3}$ and the graph on $(v_1, \ldots, v_{l-1}, v_{l+2}, v_{l+3}, \ldots, v_n)$ can be quenched.

  • a) Find a graph on four vertices that is quenchable although it is $3$-chromatic.
  • b) Construct clauses that are satisfiable if and only if a given graph is quenchable. Hint: Use the following three kinds of variables for this model-checking problem:

$x_{t,i,j} = [v_i \to v_j \text{ at time } t]$, for $1 \le i < j \le n-t$; $q_{t,k} = [\text{a quenching move of type (ii) leads to time } t+1]$; $s_{t,l} = [\text{a quenching move of type (iii) leads to time } t+1]$.

Verified: no
Solve time: 3m39s


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