| Affiliation: | (1) Division of Engineering and Applied Sciences, Harvard University and Laboratory for Computer Science Massachusetts Institute of Technology, Cambridge, MA, USA;(2) Computer Science & Engineering Department, University of California, San Diego, 0114, 9500 Gilman Drive, La Jolla, CA 92093, USA;(3) School of Mathematics, Institute for Advanced Study, Princeton, NJ, USA;(4) Hebrew University, Jerusalem, Israel |
| Abstract: | We present the best known separation between tree-like and general resolution, improving on the recent exp(n  ) separation of [2]. This is done by constructing a natural family of contradictions, of size n, that have O(n)-size resolution refutations, but only exp( (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 on some inputs, while other simple procedures, that produce general resolution refutations, will have polynomial run-time on these very same inputs. We show, furthermore that the gap we present is nearly optimal. Specifically, 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)).* This research was supported by Clore Foundation Doctoral Scholarship. Research supported by NSF Award CCR-0098197 and USA–Israel BSF Grant 97-00188. This research was supported by grant number 69/96 of the Israel Science Foundation, founded by the Israel Academy for Sciences and Humanities. |
