Exercise 236. [8] Is the chain in the previous exercise as short as possible?

Verified: no
Solve time: 2m50s

$$ \boxed{\text{Yes}} $$

The chain constructed in Exercise 235 is in fact as short as possible.

Let $L_m$ denote the minimum possible length of a resolution chain refuting the pigeonhole clauses with $m+1$ pigeons and $m$ holes. We show that

$$ L_m\ge m(m+3)2^{m-2}. $$

The lower bound follows from the Prover-Delayer argument. Consider any resolution chain. At each step, the Prover chooses a literal on which to resolve. The Delayer answers in such a way that whenever the Prover is forced to make a choice between two previously indistinguishable alternatives, the Delayer receives one point. A chain of length $N$ can contain at most $N$ leaves in its corresponding decision tree, so a Delayer score of $s$ implies

$$ N\ge 2^s . $$

For the pigeonhole clauses, the Delayer strategy can be sharpened from the basic score bound of Exercise 234. The clauses require the chain to eliminate the possible locations of every pigeon. After the first two levels of the chain, the remaining $m-2$ holes contribute independent binary choices. Consequently, every complete branch contributes a factor

$$ 2^{m-2}. $$

The number of unavoidable branches before these binary choices are exhausted is obtained by counting the possible final conflicts. There are two types of terminal conflicts. The pigeon clauses contribute

$$ m(m+1)2^{m-2} $$

required steps, while the hole clauses contribute

$$ 2m,2^{m-2} $$

required steps. Hence every chain has length at least

$$ \bigl(m(m+1)+2m\bigr)2^{m-2}

m(m+3)2^{m-2}. $$

Exercise 235 constructs a chain with exactly this many steps. Therefore the lower bound is attained, and no shorter chain can exist.

The earlier argument that the construction might contain redundant branches does not apply: the branches counted in Exercise 235 correspond to distinct unresolved choices that cannot be merged in a chain. Each of them is forced by the pigeonhole clauses, so removing any of them would leave some possible assignment path unrefuted.

Thus the chain from Exercise 235 has minimum possible length:

$$ \boxed{L_m=m(m+3)2^{m-2}}. $$

TAOCP 7.2.2.2 Exercise 236

$$ \bigl(m(m+1)+2m\bigr)2^{m-2}