Limitations Of Resolution
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)