Well known classes of boolean formulas that require exponentially long resolution proofs
Hard instances for resolution:


Tseitin's formulas (over expander graphs).
Weak ($ m $ to $ n$) pigeonhole principle (exponential in $n$ lower bounds, for any $ m>n $).
Random 3CNF's with $ n $ variables and $ O(n^{1.5-\epsilon})$ clauses, for $ 0&lt;\epsilon&lt;1/2 $.


Good, relatively up-to-date, technical survey for proof complexity lower bounds, see:

Nathan Segerlind: The Complexity of Propositional Proofs. Bulletin of Symbolic Logic 13(4): 417-481 (2007) available at: http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps