# A variation of propositional pigeonhole principle

Let $$n$$ be the number of pigeons, and $$x_{i,j}$$ denote the Boolean variable indicating that pigeon #$$i$$ is mapped to hole #$$j$$. Then the propositional pigeonhole principle (PHP) is the conjunction of following clauses:

1. $$x_{i1}\lor x_{i2}\lor\cdots\lor x_{i,n-1}$$, $$\forall 1\le i\le n$$ (a pigeon must be mapped to at least one hole)
2. $$\neg x_{ik}\lor\neg x_{jk}$$, $$\forall 1\le i (two pigeons $$i,j$$ cannot be mapped to the same hole $$k$$)

We know that the PHP formula is unsatisfiable. The reason why we can use "a pigeon must be mapped to at least one hole" instead of "a pigeon must be mapped to exactly one hole" is that, if a pigeon occupies multiple holes, then the remaining pigeons are even "less" likely to be accommodated. Now we consider replacing each $$\neg x_{i1}\lor\neg x_{j1}$$ with $$\neg x_{i1}\lor\bigvee\limits_{t=2}^{n-1}x_{it}\lor\neg x_{j1}\lor\bigvee\limits_{u=2}^{n-1}x_{ju}$$ (Note that the loosened constraints only apply to hole #1; otherwise the formulas would be satisfiable). After this, the formula is still unsatisfiable, since albeit the conditions are loosen, those $$x_{it}$$'s and $$x_{ju}$$'s can't be really set to true, because otherwise there will be no enough holes for the remaining pigeons. More intuitively, the replacement allows us to map pigeons #$$i,j$$ to the same hole #$$k$$ at the expense of mapping at least one of #$$i,j$$ simultaneously to another hole. Since a pigeon occupies at least two holes, the number of holes is still not enough so the contradiction still persists.

We know that the original PHP has a polynomial-size Frege proof saying that "from condition #1 we can infer that at least $$n$$ variables are satisfied, but from #2 we infer that at most $$n-1$$ variables are satisfied, which leads to contradiction". My question is, in this case, can we still construct a polynomial-size Frege proof for the modified formula?

update: I found that the constraints can be furthur loosened while preserving unsatisfiability. In this case we replace each $$\neg x_{ik}\lor\neg x_{jk}$$ with $$\neg x_{ik}\lor\bigvee\limits_{t=k+1}^{n-1}x_{it}\lor\neg x_{jk}\lor\bigvee\limits_{u=k+1}^{n-1}x_{ju}$$ (this time constraints for all holes for loosened, unlike in the first case where only constraints for hole #1 is loosened). This makes the formulas even harder to prove, since now the problem will not degenerate to vanilla PHP when we set some variables to true. The intuitive reason for the unsatisfiability is similar: if we let two pigeons occupy the same hole, at least one of them must also occupy another hole whose index is greater than the current one, so that the the number of holes is still not sufficient (this ordering constraint rules out the counterexample given by Joshua). Also, I used Python and PySAT to verify the unsatisfiability of these formulas and it turned out that they're still unsatisfiable up to $$n=10$$.

• I think it is now satisfiable. e.g. in the case n=3 you can set $x_{11}, x_{12}, x_{21}, x_{32}$ to 1 and the others to 0. The point is, once pigeon 1 is in two holes, at least one other pigeon is free to join it in each hole (according to these new axioms), and I believe this generalizes to any n. Dec 5, 2023 at 2:28
• @JoshuaGrochow However, $x_{12}$ and $x_{32}$ can't be both true, since the conditions are loosen just for hole 1 but not for hole 2.
– Soha
Dec 5, 2023 at 3:43
• @JoshuaGrochow Also, I've written a Python script with SAT solvers to generate the modified PHP formulas and test satisfiability, and it turned out that up to $n=10$ the formulas are still unsatisfiable.
– Soha
Dec 5, 2023 at 3:45
• You should state explicitly in the question that the loosened clause is only applied to one hole, this is unexpected. Dec 5, 2023 at 8:03
• @EmilJeřábek Sorry for the confusion. I've added clarification.
– Soha
Dec 5, 2023 at 9:07

Even the “further loosened” version has short Frege (in fact, $$\mathrm{TC}^0$$-Frege) refutations.
This argument is straightforward to formalize in Frege. Let $$\let\LOR\bigvee\xi_{ij}=x_{ij}\land\neg\LOR_{k>j}x_{ik}.$$ There are polynomial-size constant-depth Frege proofs of $$\tag{*}\LOR_jx_{ij}\to\LOR_j\xi_{ij}.$$ Indeed, putting $$\delta_{ij}=\bigvee_{k\ge j}x_{ik}$$, a simple manipulation of the definition of $$\xi_{ij}$$ yields $$\delta_{ij}\to\delta_{i,j+1}\lor\xi_{ij}.$$ Chaining these proofs together gives $$\delta_{i1}\to\delta_{in}\lor\LOR_j\xi_{ij},$$ which yields $$(*)$$ as $$\delta_{in}$$ is a falsity (empty disjunction).
Now, using $$(*)$$, clause 1 of your pigeonhole principle yields $$\LOR_j\xi_{ij}$$ for each $$i$$, and the “loosened” clause 2 gives $$\neg\xi_{ik}\lor\neg\xi_{jk}$$ for each $$i\ne j$$ and $$k$$. Thus, we can derive a contradiction using a substitution instance of the usual pigeonhole principle.