TAOCP 7.2.2.2 Exercise 237
Let the pigeonhole clauses (106) and (107) be the usual formulation of the assertion that $m+1$ pigeons cannot be placed injectively into $m$ holes.
Section 7.2.2.2: Satisfiability
Exercise 237. [28] Show that a polynomial number of steps suffice to refute the pigeonhole clauses (106), (107), if the extended resolution trick is used to append new clauses.
Verified: no
Solve time: 1m59s
Setup
Let the pigeonhole clauses (106) and (107) be the usual formulation of the assertion that $m+1$ pigeons cannot be placed injectively into $m$ holes. Let $x_{ij}$ denote the variable that is true when pigeon $i$ is placed in hole $j$, where
$$ 1\le i\le m+1,\qquad 1\le j\le m . $$
The clauses (106) assert that every pigeon occupies some hole,
$$ x_{i1}\vee x_{i2}\vee\cdots\vee x_{im}, \qquad 1\le i\le m+1, $$
and the clauses (107) assert that two distinct pigeons cannot occupy the same hole,
$$ \bar{x}{ij}\vee \bar{x}{kj}, \qquad 1\le i<k\le m+1,\quad 1\le j\le m . $$
A resolution proof requires a long chain, as constructed in exercise 235. The purpose here is to show that extended resolution permits the introduction of auxiliary variables and reduces the proof length to a polynomial in $m$.
The extended resolution rule allows a new variable $y$ to be introduced together with the defining clauses
$$ y\leftrightarrow A $$
for a previously existing formula $A$. We shall introduce variables that represent partial sums of the pigeon locations.
Solution
For $1\le j\le m$ and $1\le i\le m+1$, define extension variables
$$ y_{ij} $$
to mean that among pigeons $1,\ldots,i$ at least one pigeon occupies hole $j$. Introduce these variables by the recurrence
$$ y_{1j}\leftrightarrow x_{1j}, $$
and, for $2\le i\le m+1$,
$$ y_{ij}\leftrightarrow (y_{i-1,j}\vee x_{ij}). $$
Each definition is added by a constant number of extension-resolution steps. In particular, the equivalence
$$ y_{ij}\leftrightarrow (y_{i-1,j}\vee x_{ij}) $$
is represented by the clauses
$$ \bar y_{ij}\vee y_{i-1,j}\vee x_{ij}, $$
$$ \bar y_{i-1,j}\vee y_{ij}, $$
$$ \bar x_{ij}\vee y_{ij}. $$
The number of such clauses is proportional to the number of pairs $(i,j)$, namely
$$ m(m+1), $$
so the total number of extension clauses is $O(m^2)$.
The variables $y_{ij}$ allow the proof to express the pigeonhole counting argument recursively. Since every pigeon occupies a hole, the first pigeon gives
$$ y_{1,1}\vee y_{1,2}\vee\cdots\vee y_{1,m}. $$
Assume that after processing pigeons $1,\ldots,i$, the clauses assert that at least $i$ holes are occupied. The defining clauses for $y_{i+1,j}$ propagate this information to the next level. If pigeon $i+1$ occupies a hole already represented by some $y_{ij}$, then the clauses (107) give a contradiction. Therefore the only way to continue is to introduce a new occupied hole.
After processing all $m+1$ pigeons, the auxiliary variables imply that at least $m+1$ distinct holes are occupied. The holes are only
$$ 1,2,\ldots,m, $$
so one hole must be counted twice. Let the repeated hole be $j$, with pigeons $r$ and $s$, where $r<s$. The clauses (107) contain
$$ \bar{x}{rj}\vee\bar{x}{sj}. $$
The recurrence defining the $y$ variables derives that both $x_{rj}$ and $x_{sj}$ must be true in this situation, producing the empty clause.
The propagation through the $y_{ij}$ variables is performed once for each pair $(i,j)$ and once for each pigeon-hole exclusion clause needed in the final collision argument. There are
$$ m(m+1) $$
extension variables and at most
$$ m(m+1)+m(m+1)^2 $$
resolution steps in the complete construction. This quantity is bounded by
$$ O(m^3). $$
Thus the extended-resolution proof has polynomial length, whereas the ordinary resolution proof from exercise 235 has length
$$ m(m+3)2^{m-2}, $$
which is exponential in $m$.
This completes the proof.
∎
Verification
The auxiliary variables do not change satisfiability, because every extension variable is constrained by clauses that force it to have exactly the value of its defining formula. Therefore any assignment satisfying the original pigeonhole clauses extends uniquely to the new variables, and any contradiction derived with the new variables is also a contradiction of the original clauses.
The construction introduces $m(m+1)$ variables $y_{ij}$. Each variable has a definition involving only one previous auxiliary variable and one original variable, so every definition requires a constant number of clauses. The total size of the extension part is therefore quadratic.
The final contradiction depends only on the fact that $m+1$ pigeons require $m+1$ distinct occupied holes while only $m$ holes exist. The auxiliary variables encode this counting argument without enumerating all possible assignments. The resulting proof length is bounded by a polynomial function of $m$.
Notes
The construction is an instance of the general role of extended resolution in proof complexity. The added variables act as abbreviations for intermediate formulas, allowing a short proof to represent information that ordinary resolution must repeat many times.