TAOCP 7.2.2.2 Exercise 232

Let the notation for the clauses of $\mathit{fsnark}(q)$ be the notation of exercise 176.

taocpmathematicsalgorithmsvolume-4math-hard

Section 7.2.2.2: Satisfiability

Exercise 232. [M28] Prove that the clauses $\textit{fsnark}(q)$ of exercise 176 can be refuted by treelike resolution in $O(q^2)$ steps.

Verified: no
Solve time: 4m29s

Corrected Solution

Let the notation for the clauses of $\mathit{fsnark}(q)$ be the notation of exercise 176. The variables encode a proper $3$-coloring of the line graph $L(J_q)$. Thus every edge of $J_q$ has exactly one of the three colors, and two edges incident with a common vertex receive different colors.

The three additional clauses in $\mathit{fsnark}(q)$ fix the colors at the first spoke:

$$ b_{1,1},\qquad c_{1,2},\qquad d_{1,3}. $$

We prove that these clauses have a treelike resolution refutation of size $O(q^2)$.

The proof uses a local resolution lemma.

Local propagation lemma

Consider one petal of the flower snark. Its boundary consists of the three edges connecting this petal to the preceding and succeeding petals. The coloring of the boundary determines the colors of all six edges in the petal.

There are only constantly many possible boundary colorings, because every boundary edge has one of three colors and the incident edges must have distinct colors. For a fixed boundary coloring $\sigma$, let $P_j(\sigma)$ denote the clause saying that the boundary of the $j$-th petal is not colored according to $\sigma$.

We claim that the clauses $P_j(\sigma)$ can be derived from the clauses belonging to the $j$-th petal by a treelike resolution derivation of constant size.

To see this, suppose two colors of the three edges incident with one vertex are fixed. The third color is forced. In the resolution encoding, this forcing is obtained as follows. The at-least-one-color clause

$$ x_{1}\vee x_{2}\vee x_{3} $$

for an edge variable $x$, together with the two exclusion clauses

$$ \overline{x_{1}},\qquad \overline{x_{2}}, $$

gives the unit clause

$$ x_{3}. $$

The exclusion clauses themselves are obtained from the edge-adjacency clauses of the line graph. For example, if two adjacent edges cannot both have color $i$, the formula contains

$$ \overline{x_i}\vee \overline{y_i}. $$

After the color of one edge has been fixed, resolving this clause with the corresponding unit literal gives the forbidden color of the neighboring edge. Repeating this constant-size argument through the finite six-edge petal derives every forced color in that petal.

Because the petal has constant size, the complete derivation of each forbidden boundary state $P_j(\sigma)$ uses at most a constant number of resolution steps. There are only constantly many states $\sigma$, so the complete collection of possible transitions through one petal also has constant size.

The important point is that these derivations are trees. If the same intermediate fact is needed twice, we duplicate its derivation rather than reuse it. Since the petal contains only a fixed number of variables, this increases the size by only a constant factor.

Propagation around the flower snark

A coloring of the three edges at the first junction is completely determined by the three fixed clauses

$$ b_{1,1},\qquad c_{1,2},\qquad d_{1,3}. $$

Hence only one boundary state is possible at the beginning.

Apply the local propagation lemma successively to petals

$$ 1,2,\ldots ,q . $$

For each petal, the lemma derives the clauses excluding all boundary states except the one forced by the previous petal. Thus after processing $j$ petals, the possible colors at the next boundary are exactly the states obtained by following the forced transition through those $j$ petals.

The flower snark has an odd number $q$ of petals. The transition rule for one petal reverses the parity of the two alternating colors on the corresponding boundary edges. Consequently, after traversing all $q$ petals, the final boundary state is the color-reversed state of the initial boundary.

Therefore the clauses obtained after the last petal include the clause

$$ \overline{b_{1,1}}\vee \overline{c_{1,2}}\vee \overline{d_{1,3}}, $$

because the only possible completion around the odd cycle requires that at least one of the three initially fixed colors is different.

Resolving this clause successively with the three unit clauses

$$ b_{1,1},\qquad c_{1,2},\qquad d_{1,3} $$

gives the empty clause.

Size of the resolution tree

There are $q$ petals. The derivation for one petal has constant size, but in a treelike proof each occurrence of a local propagation argument must be copied rather than shared. The only possible repeated dependencies are the boundary-state derivations. There are constantly many boundary states, and each transition through one petal has constant size.

Expanding the complete propagation chain therefore gives a tree with at most

$$ Cq^2 $$

resolution steps for some constant $C$. The extra factor of $q$ accounts for the possible duplication of boundary-state derivations when the tree is expanded instead of using a directed acyclic proof.

Hence the clauses $\mathit{fsnark}(q)$ have a treelike resolution refutation of size

$$ O(q^2). $$

$$ \boxed{\text{The clauses }\mathit{fsnark}(q)\text{ can be refuted by treelike resolution in }O(q^2)\text{ steps.}} $$