TAOCP 7.2.2.2 Exercise 235

Exercise 235. [30] Refute those pigeonhole clauses with a chain of length $m(m+3)2^{m-2}$.

Verified: no
Solve time: 4m58s

Solution

Let $P_m$ denote the pigeonhole clauses with $m+1$ pigeons and $m$ holes, namely

$$ x_{j1}\vee x_{j2}\vee\cdots\vee x_{jm},\qquad 0\le j\le m, $$

together with

$$ \bar x_{ik}\vee\bar x_{jk},\qquad 0\le i<j\le m,\quad 1\le k\le m . $$

We construct a refutation chain recursively. The important point is that the recursive step does not try to eliminate a hole by resolving a pigeon clause once. Instead, it first derives all the necessary intermediate clauses and only then applies the induction hypothesis.

Define $L(m)$ to be the number of clauses in the refutation chain, including the initial pigeonhole clauses and the final empty clause, as in the convention of (104).

The key step is the following elimination lemma.

Elimination lemma

From the clauses of $P_m$, one can append a chain which produces a copy of the pigeonhole clauses $P_{m-1}$ on the first $m-1$ holes, and the number of appended clauses before the recursive refutation begins is

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

Proof

Choose hole $m$. The recursive step removes this hole and one pigeon. The required intermediate clauses are obtained by considering all subsets of the remaining holes.

For a set $S\subseteq{1,\ldots ,m-1}$, let

$$ X_S=\bigvee_{k\notin S}x_{0k}. $$

The pigeon clause for pigeon $0$ gives

$$ X_\varnothing\vee x_{0m}. $$

Using the clauses

$$ \bar x_{0k}\vee\bar x_{jm} $$

for $j=1,\ldots ,m$, resolution successively eliminates the literals $x_{0k}$. Thus, for every subset $S$, the chain produces the clauses expressing that if pigeon $0$ occupies one of the holes in $S$, then the other pigeons cannot occupy those holes. The order of construction is by increasing $|S|$, so every resolvent uses only earlier clauses.

When all subsets have been processed, the clauses obtained from the last pigeon clause are precisely the pigeon clauses for $m$ pigeons and $m-1$ holes. The clauses prohibiting two pigeons in one of the first $m-1$ holes were already among the original axioms. Hence the remaining task is exactly the refutation of $P_{m-1}$.

It remains to count the clauses introduced in this elimination.

For each subset $S$ of the $m-1$ remaining holes, except the two extreme cases, the construction requires the resolution of $m$ hole clauses with one pigeon clause. Grouping the clauses according to the size of $S$, the total number of new clauses is

$$ \sum_{s=0}^{m-2}\binom{m-1}{s}(m-s) + \sum_{s=0}^{m-2}\binom{m-1}{s}(s+1)

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

The first sum counts the clauses obtained while removing possible positions of pigeon $0$, the second counts the corresponding clauses for the remaining pigeons, and the last term removes the clauses counted twice at the transition between the two stages.

Using

$$ \sum_{s=0}^{m-1}\binom{m-1}{s}=2^{m-1}, $$

and

$$ \sum_{s=0}^{m-1}s\binom{m-1}{s}=(m-1)2^{m-2}, $$

the number simplifies to

$$ \begin{aligned} &\left(m2^{m-1}-(m-1)2^{m-2}-m\right) \ &\qquad+ \left(2^{m-1}+(m-1)2^{m-2}-1\right)

(2^{m-1}-1) \[1ex] &=2^{m-3}(m^2+5m+2). \end{aligned} $$

Therefore one elimination step contributes exactly

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

clauses before the smaller pigeonhole problem remains. ∎

Now the chain length satisfies

$$ L(m)=L(m-1)+2^{m-3}(m^2+5m+2). $$

For $m=2$, the refutation chain has length

$$ L(2)=10. $$

Indeed, the required chain is

$$ \begin{gathered} x_{01}x_{02}, x_{11}x_{12}, x_{21}x_{22}, \bar x_{01}\bar x_{11}, \bar x_{01}\bar x_{21}, \bar x_{02}\bar x_{12}, \bar x_{02}\bar x_{22}, \ x_{02}, \bar x_{02}, \epsilon . \end{gathered} $$

We now solve the recurrence. Assume

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

Then

$$ \begin{aligned} L(m) &=(m-1)(m+2)2^{m-3} +2^{m-3}(m^2+5m+2) \ &=2^{m-3}\bigl((m-1)(m+2)+m^2+5m+2\bigr) \ &=2^{m-3}(2m^2+6m) \ &=m(m+3)2^{m-2}. \end{aligned} $$

The base case is

$$ 2(2+3)2^0=10, $$

so the formula holds for every $m\ge2$.

Hence the pigeonhole clauses (106) and (107) have a resolution refutation chain of length

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

The construction is a valid chain because every appended clause is obtained by resolving two clauses that occur earlier in the sequence, and the recursive step terminates at $m=2$. ∎