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

  • $\begingroup$ 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 $\endgroup$
    – Chris Beck
    Oct 21, 2018 at 17:38

1 Answer 1


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.

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,

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.