<p>It’s amazing that your question matches the papers I have recently read. For Tseitin formulas, there are papers that obtain regular resolution lower bounds from corresponding read-once branching programs.</p>
<ul>
<li>Itsykson D, Riazanov A, Sagunov D, et al. <a href="https://www.semanticscholar.org/paper/Almost-Tight-Lower-Bounds-on-Regular-Resolution-of-Itsykson-Riazanov/13fc1895275ba6dcac64aca067ef97801d37badf" rel="nofollow noreferrer">Almost Tight Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs</a>[C]//Electron. Colloquium Comput. Complex. 2019, 26: 178.</li>
<li>de Colnet, Alexis, and Stefan Mengel. &quot;<a href="https://www.jair.org/index.php/jair/article/view/13521" rel="nofollow noreferrer">Characterizing Tseitin-formulas with short regular resolution refutations.</a>&quot; Journal of Artificial Intelligence Research 76 (2023): 265-286.</li>
<li>Itsykson, Dmitry, Artur Riazanov, and Petr Smirnov. &quot;<a href="https://drops.dagstuhl.de/opus/volltexte/2022/16680/" rel="nofollow noreferrer">Tight Bounds for Tseitin Formulas.</a>&quot; 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2022.</li>
</ul>
<p>However, their transformation depends on the special structure of Tseitin formulas, I have no idea if pigeonhole can apply this approach.</p>
<p>For <span class="math-container">$PHP_n^{n+1}$</span>,
Maybe this will help,</p>
<ul>
<li>Ben-Sasson, Eli, and Avi Wigderson. &quot;<a href="https://www.researchgate.net/publication/2370656_Short_Proofs_are_Narrow_-_Resolution_made_Simple" rel="nofollow noreferrer">Short proofs are narrow—resolution made simple.</a>&quot; Proceedings of the thirty-first annual ACM symposium on Theory of computing. 1999.</li>
</ul>
<p>Eli Ben-Sasson and Avi Wigderson give a more simple proof of <span class="math-container">$PHP_n^{n+1}$</span> by proving the width of resolution will be large.</p>
<p>By the way, I am also searching for more unsatisfiable examples that get regular resolution lower bound directly from read-once branching programs. If you know more, please tell me.</p>

CC BY-SA 4.0
2023-04-20T06:35:01.343Z
2023-04-21T01:31:18.503Z
2023-04-21T01:31:18.503Z
Jxb
<p>It is well known that the pigeonhole principle <span class="math-container">$PHP_n^{n+1}$</span> is hard for general resolution. The original proof due to Haken is elegant. One first defines a complexity measure for derived clauses, in which axioms have low complexity, and the final empty clause has high complexity. Then one shows that clauses of medium complexity must have many literals. Finally, one shows that if <span class="math-container">$\Pi$</span> is a refutation of small size, then one can restrict the values of some variables in such a way that the resulting formula <span class="math-container">$PHP_{n-k}^{n-k+1}$</span> has a corresponding refutation <span class="math-container">$\Pi'$</span> of width smaller than what it should be. Contradiction. </p>

<p>Regular resolution is the special case of resolution where variables are not allowed to be resolved more than once in any path from an axiom to the final empty clause. It is well known that regular resolution refutations are essentially read-once branching programs. </p>

<p>Is there a well known way of proving that <span class="math-container">$PHP_n^{n+1}$</span> is hard for <em>regular</em> resolution directly, without using Haken's arguments? I would imagine that since regular resolution proofs correspond to read-once branching programs, one could actually use a more direct approach based on rectangle covers and so on. Is this intuition right? Are there any discussions of this technique in the literature? </p>

<p>Ps: I'm aware of a <a href="https://link.springer.com/article/10.1007/s00493-004-0030-y" rel="noreferrer">paper</a> due to Pitassi and Raz, which shows that the <em>weak</em> pigeonhole principle is hard for regular resolution. But now this proof is probably much more complicated than a proof for the original <span class="math-container">$PHP_n^{n+1}$</span> tautologies due to the <em>weak</em> modification.</p>

CC BY-SA 4.0
2018-10-21T17:38:40.893Z
I haven't read such a paper, but I think that such a proof outline can likely work out. I wrote a paper with Paul Beame and Russell Impagliazzo in 2012 about Time Space tradeoffs in Tseitin tautologies. Your question isn't about tradeoffs, but one technique we gave does give a sharp lower bound (for regular resolution) for Tseitin taulogies, showing that at least $2^{(w-1)}$ medium complexity clauses are required for Tseitin tautologies on a grid of width w, matching the ~ $2^w$ upper bound pretty closely. For your question I would consider adapting the "probabilistic adversary" approach
Chris Beck
<resolution>
Direct Proof that the Pigeonhole Principle is Hard for Regular Resolution
corregular
# Direct Proof that the Pigeonhole Principle is Hard for Regular Resolution

(Asked by: username_0 on 2018-10-17)

It is well known that the pigeonhole principle $PHP\_n^{n+1}$ is hard for general resolution. The original proof due to Haken is elegant. One first defines a complexity measure for derived clauses, in which axioms have low complexity, and the final empty clause has high complexity. Then one shows that clauses of medium complexity must have many literals. Finally, one shows that if $\Pi$ is a refutation of small size, then one can restrict the values of some variables in such a way that the resulting formula $PHP\_{n-k}^{n-k+1}$ has a corresponding refutation $\Pi'$ of width smaller than what it should be. Contradiction.

Regular resolution is the special case of resolution where variables are not allowed to be resolved more than once in any path from an axiom to the final empty clause. It is well known that regular resolution refutations are essentially read-once branching programs.

Is there a well known way of proving that $PHP\_n^{n+1}$ is hard for *regular* resolution directly, without using Haken's arguments? I would imagine that since regular resolution proofs correspond to read-once branching programs, one could actually use a more direct approach based on rectangle covers and so on. Is this intuition right? Are there any discussions of this technique in the literature?

Ps: I'm aware of a [paper](https://link.springer.com/article/10.1007/s00493-004-0030-y) due to Pitassi and Raz, which shows that the *weak* pigeonhole principle is hard for regular resolution. But now this proof is probably much more complicated than a proof for the original $PHP\_n^{n+1}$ tautologies due to the *weak* modification.

**Tags:** resolution
> **Comments:**
> **username_1**: I haven't read such a paper, but I think that such a proof outline can likely work out. I wrote a paper with Paul Beame and Russell Impagliazzo in 2012 about Time Space tradeoffs in Tseitin tautologies. Your question isn't about tradeoffs, but one technique we gave does give a sharp lower bound (for regular resolution) for Tseitin taulogies, showing that at least $2^{(w-1)}$ medium complexity clauses are required for Tseitin tautologies on a grid of width w, matching the ~ $2^w$ upper bound pretty closely. For your question I would consider adapting the "probabilistic adversary" approach  

---

## 1 answers

### Answer by username_2 on 2023-04-20. Score: 2

It’s amazing that your question matches the papers I have recently read. For Tseitin formulas, there are papers that obtain regular resolution lower bounds from corresponding read-once branching programs.

* Itsykson D, Riazanov A, Sagunov D, et al. [Almost Tight Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs](https://www.semanticscholar.org/paper/Almost-Tight-Lower-Bounds-on-Regular-Resolution-of-Itsykson-Riazanov/13fc1895275ba6dcac64aca067ef97801d37badf)[C]//Electron. Colloquium Comput. Complex. 2019, 26: 178.
* de Colnet, Alexis, and Stefan Mengel. "[Characterizing Tseitin-formulas with short regular resolution refutations.](https://www.jair.org/index.php/jair/article/view/13521)" Journal of Artificial Intelligence Research 76 (2023): 265-286.
* Itsykson, Dmitry, Artur Riazanov, and Petr Smirnov. "[Tight Bounds for Tseitin Formulas.](https://drops.dagstuhl.de/opus/volltexte/2022/16680/)" 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2022.

However, their transformation depends on the special structure of Tseitin formulas, I have no idea if pigeonhole can apply this approach.

For $PHP\_n^{n+1}$,
Maybe this will help,

* Ben-Sasson, Eli, and Avi Wigderson. "[Short proofs are narrow—resolution made simple.](https://www.researchgate.net/publication/2370656_Short_Proofs_are_Narrow_-_Resolution_made_Simple)" Proceedings of the thirty-first annual ACM symposium on Theory of computing. 1999.

Eli Ben-Sasson and Avi Wigderson give a more simple proof of $PHP\_n^{n+1}$ by proving the width of resolution will be large.

By the way, I am also searching for more unsatisfiable examples that get regular resolution lower bound directly from read-once branching programs. If you know more, please tell me.


---

