3
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ So do you find some alternative proofs more readable? If any, could you please share with me. $\endgroup$
    – Jxb
    Apr 20, 2023 at 8:45

2 Answers 2

4
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Although I am not the questioner, your answer also solved my confusion. When I searched for the result of obtaining the resolution size through width, I only found the applications of Tseitin formula and Pigeonhole. May I ask if you know the application of this method in other formulas? $\endgroup$
    – Jxb
    Apr 11, 2023 at 3:07
  • 1
    $\begingroup$ Check the papers citing Ben-Sasson–Wigderson. $\endgroup$ Apr 11, 2023 at 19:38
1
$\begingroup$

I would recommend "Proofs as Games" by Pavel Pudlak. I find the prover-adversary model quite useful for building intuition. For example, soundness and completeness of resolution are trivial (Prover just queries all variables). It has been used, for example, in "Planar tautologies are hard for resolution" by Dantchev and Riis.

Although resolution width unified many previous lower bounds, it does not capture all of them. In particular, it cannot show lower bounds on formulas that start with a wide clause. "Random restriction" is the more general approach.

$\endgroup$

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.