文章基本信息

标题：Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems
本地全文：下载
作者：Maria Luisa Bonet ; Juan Luis Esteban ; Nicola Galesi 等
期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：1998
卷号：1998
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：We prove an exponential lower bound for tree-like Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential separation between tree-like and dag-like proofs for both Cutting Planes and resolution; in both cases only superpolynomial separations were known before. In order to prove this, we extend the lower bounds on the depth of monotone circuits of Raz and McKenzie (FOCS 97) to monotone real circuits. In the case of resolution, we further improve this result by giving an exponential separation of tree-like resolution from (dag-like) regular resolution proofs. In fact, the refutation provided to give the upper bound respects the stronger restriction of being a Davis-Putnam resolution proof. This extends the corresponding superpolynomial separation of Urquhart (BSL 1995). Finally, we prove an exponential separation between Davis-Putnam resolution and unrestricted resolution proofs; only a superpolynomial separation was previously known (Goerdt, Ann. Math. AI 1992).
关键词：CuttingPlanes, Davis-Putnam resolution, lower bound, Propositional Proof System, regular resolution, Resolution, tree-like proofs Abstract: