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.
