I'm trying to gain an intuitive understanding of why propositional resolution proofs tend to be so long.
As every essential prime implicant can be produced via resolution, intuitively I would have guessed that lower bounds on the length of resolution would be left open, or perhaps even equivalent to whether NP = co-NP. However, it is proven that resolution proofs can have exponential lower bounds, as shown by Tseitin's and Haken's work on the pigeonhole principle.
This establishes resolution as being a lot less useful than one would hope, and indeed this is so well known that modern solvers look at all manner of other refutation proofs.
Trying a resolution proof on a pigeonhole principle formula quickly yields an explosion of mostly useless clauses with tons of literals, but I don't exactly understand why this is the case.
Is there some ultra-simple example that can illustrate where resolution goes wrong, or provide some intuition for why auxiliary variables can (at least sometimes) rectify this issue?