Limitations Of Resolution
Method can’t “count”! Pigeon-hole formulas: Can’t place N+1 objects in N holes. Shortest resolution proof is exponentially long. (Cook / Karp 1972; Haken 1985)
Random unsat formulas: exponential size proofs.
Explains why we can’t push DP over 400 vars:
400 vars requires search tree of about 10 million nodes
1000 vars unsat requires 10^15 nodes! (Chvatal and Szemeredi 1988; Crawford 1995)