Does SAT always have short analytic proofs? By analytic proof, I mean mainly resolution and also other valid syntactical manipulations of the set of clauses, old and new. So this is a search over problem space rather than solution space. The question is:

Is there a family of instances of SAT that doesn't have polynomial-size analytic proofs of their satisfiabilities?

If all families have short analytic proofs, then if we can find them in short time, that means P = NP. But even if there aren't always, there still may be other means to solve SAT in polynomial-time. So this is only one way to attack P vs. NP. But it's curious to know on its own.
It is known that proofs of the unsatisfiability of pigeonhole problems must be at least length $2^{n^\epsilon}$ when the resolution proof system is used.  $\epsilon$ depends on the difference between the number of pigeons and the number of holes, but $\epsilon &gt; 0$ always.