<p>Even the “further loosened” version has short Frege (in fact, <span class="math-container">$\mathrm{TC}^0$</span>-Frege) refutations.</p>
<p>Why is the principle unsatisfiable in the first place? Because if you map each pigeon to the hole with <em>maximal index</em> to which it is assigned by the original assignment, the “loosened clause” guarantees that the mapping is injective, hence it violates standard PHP.</p>
<p>This argument is straightforward to formalize in Frege. Let
<span class="math-container">$$\let\LOR\bigvee\xi_{ij}=x_{ij}\land\neg\LOR_{k&gt;j}x_{ik}.$$</span>
There are polynomial-size constant-depth Frege proofs of
<span class="math-container">$$\tag{$*$}\LOR_jx_{ij}\to\LOR_j\xi_{ij}.$$</span>
Indeed, putting <span class="math-container">$\delta_{ij}=\bigvee_{k\ge j}x_{ik}$</span>, a simple manipulation of the definition of <span class="math-container">$\xi_{ij}$</span> yields
<span class="math-container">$$\delta_{ij}\to\delta_{i,j+1}\lor\xi_{ij}.$$</span>
Chaining these proofs together gives
<span class="math-container">$$\delta_{i1}\to\delta_{in}\lor\LOR_j\xi_{ij},$$</span>
which yields <span class="math-container">$(*)$</span> as <span class="math-container">$\delta_{in}$</span> is a falsity (empty disjunction).</p>
<p>Now, using <span class="math-container">$(*)$</span>, clause 1 of your pigeonhole principle yields
<span class="math-container">$$\LOR_j\xi_{ij}$$</span>
for each <span class="math-container">$i$</span>, and the “loosened” clause 2 gives
<span class="math-container">$$\neg\xi_{ik}\lor\neg\xi_{jk}$$</span>
for each <span class="math-container">$i\ne j$</span> and <span class="math-container">$k$</span>. Thus, we can derive a contradiction using a substitution instance of the usual pigeonhole principle.</p>

CC BY-SA 4.0
2023-12-06T10:16:44.187Z
2023-12-06T10:16:44.187Z
Emil Jeřábek
<p>Let <span class="math-container">$n$</span> be the number of pigeons, and <span class="math-container">$x_{i,j}$</span> denote the Boolean variable indicating that pigeon #<span class="math-container">$i$</span> is mapped to hole #<span class="math-container">$j$</span>. Then the propositional pigeonhole principle (PHP) is the conjunction of following clauses:</p>
<ol>
<li><span class="math-container">$x_{i1}\lor x_{i2}\lor\cdots\lor x_{i,n-1}$</span>, <span class="math-container">$\forall 1\le i\le n$</span> (a pigeon must be mapped to at least one hole)</li>
<li><span class="math-container">$\neg x_{ik}\lor\neg x_{jk}$</span>, <span class="math-container">$\forall 1\le i&lt;j\le n,1\le k\le n-1$</span> (two pigeons <span class="math-container">$i,j$</span> cannot be mapped to the same hole <span class="math-container">$k$</span>)</li>
</ol>
<p>We know that the PHP formula is unsatisfiable. The reason why we can use &quot;a pigeon must be mapped to at least one hole&quot; instead of &quot;a pigeon must be mapped to <em>exactly</em> one hole&quot; is that, if a pigeon occupies multiple holes, then the remaining pigeons are even &quot;less&quot; likely to be accommodated. Now we consider replacing each <span class="math-container">$\neg x_{i1}\lor\neg x_{j1}$</span> with <span class="math-container">$\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}$</span> (<em>Note that the loosened constraints only apply to hole #1; otherwise the formulas would be satisfiable</em>). After this, the formula is still unsatisfiable, since albeit the conditions are loosen, those <span class="math-container">$x_{it}$</span>'s and <span class="math-container">$x_{ju}$</span>'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 #<span class="math-container">$i,j$</span> to the same hole #<span class="math-container">$k$</span> at the expense of mapping at least one of #<span class="math-container">$i,j$</span> 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.</p>
<p>We know that the original PHP has a polynomial-size Frege proof saying that &quot;from condition #1 we can infer that at least <span class="math-container">$n$</span> variables are satisfied, but from #2 we infer that at most <span class="math-container">$n-1$</span> variables are satisfied, which leads to contradiction&quot;. My question is, in this case, can we still construct a polynomial-size Frege proof for the modified formula?</p>
<p><em>update</em>: I found that the constraints can be furthur loosened while preserving unsatisfiability. In this case we replace each <span class="math-container">$\neg x_{ik}\lor\neg x_{jk}$</span> with <span class="math-container">$\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}$</span> (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 <span class="math-container">$n=10$</span>.</p>

CC BY-SA 4.0
2023-12-05T02:28:20.133Z
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.
Joshua Grochow
CC BY-SA 4.0
2023-12-05T03:43:32.990Z
@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
CC BY-SA 4.0
2023-12-05T03:45:36.717Z
@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
CC BY-SA 4.0
2023-12-05T08:03:15.087Z
You should state explicitly in the question that the loosened clause is only applied to one hole, this is unexpected.
Emil Jeřábek
CC BY-SA 4.0
2023-12-05T09:07:10.640Z
@EmilJeřábek Sorry for the confusion. I've added clarification.
Soha
<proof-complexity>
A variation of propositional pigeonhole principle
Soha
# A variation of propositional pigeonhole principle

(Asked by: username_0 on 2023-12-05)

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$.

**Tags:** proof-complexity

> **Comments:**
> **username_1**: 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.  
> **username_0**: @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.  
> **username_0**: @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.  
> **username_2**: You should state explicitly in the question that the loosened clause is only applied to one hole, this is unexpected.  
> **username_0**: @EmilJeřábek Sorry for the confusion. I've added clarification.  

---

## 1 answers

### Answer by username_2 on 2023-12-06. Score: 4 | Accepted answer

Even the “further loosened” version has short Frege (in fact, $\mathrm{TC}^0$-Frege) refutations.

Why is the principle unsatisfiable in the first place? Because if you map each pigeon to the hole with *maximal index* to which it is assigned by the original assignment, the “loosened clause” guarantees that the mapping is injective, hence it violates standard PHP.

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.


---

