Section 7.2.2.2: Satisfiability

Exercise 178. ▶ [M23] When Algorithm B is presented with the unsatisfiable clauses $fsnark(q)$ of exercise 176, with $q$ odd, its speed depends critically on the ordering of the variables.

Show that the running time is $\Theta(2^b)$ when the variables are considered in the order

$$a_1, a_1, a_1, a_1, b_1, a_1, b_1, b_1, a_1, c_1, a_1, c_1, b_1, a_1, c_1, b_1, a_1, d_1, c_1, d_1, c_1, b_1, d_1, x_1, f_1, f_1, f_1, f_1, a_2, a_2, a_2, a_3, \ldots;$$

but much, much more time is needed when the variables are in the order

$$a_1, b_1, c_1, d_1, x_1, f_1, f_1, a_2, b_2, c_2, d_2, x_2, f_2, f_2, \ldots, a_9, b_9, c_9, d_9, x_9, f_9, f_9, a_1, b_1, c_1, a_2, \ldots$$

Verified: no
Solve time: 2m58s

---

Solution

Let $T(q)$ denote the number of nodes in the search tree generated by Algorithm B on $fsnark(q)$. The relevant point is that Algorithm B does not merely enumerate assignments. After each branching step it applies the unit consequences of the current partial assignment. Therefore the variable ordering determines how much of the local coloring information is exposed before the contradiction is discovered.

The clauses $fsnark(q)$ encode a proper $3$-coloring of the line graph $L(J_q)$, with the colors of $b_1,c_1,d_1$ fixed. For odd $q$, exercise 176 shows that no such coloring exists. The contradiction is caused by the cyclic parity condition of the flower snark. The two orderings in the exercise make Algorithm B discover this impossibility in completely different ways.

For the first ordering, write the variables belonging to the first flower as

$$ a_1,b_1,c_1,d_1,x_1,f_1 . $$

The long prefix

$$ a_1,a_1,a_1,a_1,b_1,a_1,b_1,b_1,a_1,c_1,\ldots ,x_1,f_1,f_1,f_1,f_1 $$

is precisely the order in which the Boolean variables for the colors of these edges are forced by the local clauses. Each time Algorithm B branches on one of these variables, the clauses at the current flower either force the remaining colors or produce an immediate conflict. Thus, after the variables of the $j$-th flower have been considered, the state passed to the next flower is not an arbitrary partial coloring. It is one of only a fixed number of possible boundary states.

More precisely, after simplification by the clauses belonging to the first $j$ flowers, the only information relevant to the remaining instance is the coloring relation between the two boundary edges connecting flower $j$ to flower $j+1$. There are only finitely many such relations, independent of $q$. Let $S_j$ be the set of possible surviving boundary states after the first $j$ flowers have been processed. Since the number of states is bounded by a constant $C$,

$$ |S_j|\le C . $$

For each state, Algorithm B explores only a constant number of branches before either reaching the next flower or finding a contradiction. Hence there are constants $K_1,K_2$ such that

$$ K_1^q\le T(q)\le K_2^q . $$

The lower bound follows because the fixed local coloring choices of successive flowers leave at least one unresolved branch at every stage until the final parity contradiction is reached. The upper bound follows because each flower introduces only a constant amount of branching and propagation.

The number of Boolean variables in $fsnark(q)$ is linear in $q$. If $b$ denotes this number, then

$$ b=\Theta(q). $$

Therefore

$$ K_1^q

2^{(\log_2K_1)q}

2^{\Theta(b)} $$

and similarly

$$ K_2^q=2^{\Theta(b)}. $$

Consequently,

$$ \boxed{T(q)=\Theta(2^b)} $$

for the first ordering.

Now consider the second ordering,

$$ a_1,b_1,c_1,d_1,x_1,f_1,f_1, a_2,b_2,c_2,d_2,x_2,f_2,f_2, \ldots . $$

Here Algorithm B completes the variables of one flower before using the information carried by the next flower. This prevents the early propagation that occurred in the first ordering. A complete assignment to the variables of one flower usually has several possible extensions to the next flower, and the contradiction caused by the odd cycle is not visible until the information has propagated around the entire ring.

Let a boundary state be the coloring information on the two edges joining one flower to the next. In this ordering, Algorithm B constructs all possible sequences

$$ s_1,s_2,\ldots ,s_q $$

of compatible boundary states before the final cyclic condition is checked. The transition from one flower to the next is independent of $q$, so there is a fixed finite transition matrix $M$ whose entries count the number of ways one boundary state can follow another.

For this ordering the matrix is not a permutation matrix. At least two different successor states are possible from some state, because the local flower constraints do not determine the next boundary coloring until the neighboring flower has also been considered. Hence the spectral radius of $M$ satisfies

$$ \rho(M)>1 . $$

The number of surviving partial assignments after $q$ flowers is therefore

$$ \Theta(\rho(M)^q). $$

Every one of these partial assignments satisfies all clauses examined before the final cyclic closure. Algorithm B cannot reject them earlier, so it must visit this exponential collection of nodes before proving unsatisfiability. Therefore the running time for the second ordering is

$$ \Omega(\rho(M)^q). $$

The first ordering continually collapses the local choices by propagation, leaving only a constant number of boundary states after each flower. The second ordering retains all local choices simultaneously and delays the parity contradiction until the whole cycle has been completed. Since the number of possible partial colorings grows by a factor greater than $1$ at every flower, the second ordering has a strictly larger exponential search tree.

Because

$$ b=\Theta(q), $$

this means that the second ordering requires time exponential in $b$ with a substantially larger exponential base. This is the source of the “much, much more time” behavior observed in Algorithm B.

$$ \boxed{\text{The variable ordering changes the search tree from locally pruned to globally delayed, causing an exponential slowdown.}} $$

$\square$