文章基本信息

标题：Lower Bounds on OBDD Proofs with Several Orders
本地全文：下载
作者：Sam Buss ; Dmitry Itsykson ; Alexander Knop 等
期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2020
卷号：2020
页码：1-27
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：This paper is motivated by seeking lower bounds on OBDD(∧, w, r) refutations, namely OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1-NBP(∧) refutations based on read-once nondeterministic branching programs. These generalize OBDD(∧, r) refutations. There are polynomial size 1-NBP(∧) refutations of the pigeonhole principle, hence 1-NBP(∧) is strictly stronger than OBDD(∧, r). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP(∧) refutations. As a corollary, OBDD(∧, r) does not simulate tree-like resolution, answering a previously open question. The system 1-NBP(∧, ∃) uses projection inferences instead of weakening. 1-NBP(∧, ∃k) is the system restricted to projection on at most k distinct variables. We construct explicit constant degree graphs Gn on n vertices and an > 0, such that 1-NBP(∧, ∃n) refutations of the Tseitin formula for Gn require exponential size. Second, we study the proof system OBDD(∧, w, r`) which allows ` different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD(∧, w, r`) refutations for ` = log n, where n is the number of variables and > 0 is a constant. The lower bound is based on multiparty communication complexity.