Resolution exponential lower bound... alternative proofs? I am reading the Resolution proof system exponential lower bound via Haken's bottleneck method for the Pigeonhole Principle as presented in Arora and Barak's Computational Complexity: A Modern Approach, Chapter 15. However, I don't like how the proof is presented in the book and I am having some difficulties following it.

Does somebody know of alternative sources where this same proof is presented? I know there are different techniques to show exponential lower bounds for Resolution, but I want something based on the Pigeonhole Principle. It's just that the phrasing in this book is truly confusing.
If you don't like the presentation of Arora and Barak, you can always take a look at Haken's original paper.

The modern approach to Resolution lower bounds is, however, via Resolution width, as worked out in a classical paper of Ben-Sasson and Wigderson. You can also find expositions in various lecture notes, for example by Jakob Nordström.