Near-Optimal Separation of Treelike and General Resolution
Eli Ben‐Sasson, Russell Impagliazzo, Avi Wigderson · 2000
We present the best known separation between tree-like and general resolution, improving on the recent exp(n ) separation of [BEGJ98]. This is done by constructing a natural family of contradictions, of size n, that have O(n)-size resolution refutations, but onlyexp( n= log n))- size tree-like refutations. This result implies that the most commonly used automated theorem procedures, which produce tree-like resolution refutations, will perform badly of some inputs, while other simple procedures, that produce general resolution refutations, will have polynomial runtime on these very same inputs. We show, furthermore that the gap we present is nearly optimal. Specically, if S (S T ) is the minimal size of a (tree-like) refutation, we prove that S T = exp(O(S log log S= log S)). 1 Introduction and Main Results The resolution refutation system is one of the oldest and most commonly used methods for proving the unsatisability of CNF formulas, and is interesting from a the...