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.