# Refutation of pigeonhole using resolution

I am trying to find a way to refute the pigeonhole formula using resolution.

Lets assume that $x_{ij}$ is true if $i^{th}$ pigeon is in $j^{th}$ hole.

Thus, with $n$ holes and $n+1$ pigeons, the first condition "every pigeon must be in a hole" can be represented as

$$\alpha_n = \bigwedge_{1\leq i \leq n+1} (x_{i1} \vee \dots \vee x_{in}),$$

and the second condition "no two pigeons are in same hole" can be represented as

$$\beta_n = \bigwedge_{1\leq j\leq n} \bigwedge_{1\leq i<k\leq n+1} \neg(x_{ij} \wedge x_{kj}) = \bigwedge_{1\leq j\leq n} \bigwedge_{1\leq i<k\leq n+1} (\neg x_{ij} \vee \neg x_{kj})$$

The complete piegonhole formula can be represented as $\varphi_n = \alpha_n \wedge \beta_n$.

With $n=1$, it is easy to refute $\varphi_1$ with resolution, as shown below: $$\alpha_1 = x_{11}\wedge x_{21} \\ \beta_1 = \neg x_{11}\vee \neg x_{21} \\ \varphi_1 = x_{11}\wedge x_{21} \wedge (\neg x_{11}\vee \neg x_{21}) \xrightarrow{unit-resolution} \sqcup\ (empty\ clause)$$

However, with $n\geq 2$ there is no unit-clause. For example with $n=2$, we have only 2-clauses. In that case a possible resolution of 2 clauses will produce another 2-clause.

Thus, I am wondering how to produce a refutation proof for $\varphi_{n\geq 2}$ with resolution, as we know that resolution is refutationally complete.

For reference, $\alpha_2$, and $\beta_2$ should look like below: $$\alpha_2 = (x_{11} \vee x_{12}) \wedge (x_{21} \vee x_{22}) \wedge (x_{31} \vee x_{32}) \\ \beta_2 = (\neg x_{11} \vee \neg x_{21}) \wedge (\neg x_{11} \vee \neg x_{31}) \wedge (\neg x_{21} \vee \neg x_{31}) \wedge (\neg x_{12} \vee \neg x_{22}) \wedge (\neg x_{12} \vee \neg x_{32}) \wedge (\neg x_{22} \vee \neg x_{32})$$

• Take a look at this paper: Resolution and the Weak Pigeonhole Principle by Buss and Pitassi. Another option is to use the "brute force proof" (the proof used to prove that Resolution is refutation complete), though this will be less explicit than the proof in the paper. – Yuval Filmus Jul 12 '17 at 15:16