Sam Buss, Dmitry Itsykson, Alexander Knop,
Artur Riazanov, and Dmitry Sokolov
Lower Bounds on OBDD Proofs with Several Orders
ACM Transactions on Computational Logic 22, 4, Article 26 (2021) 30 pages.
Abstract: 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 ε is a constant. The lower bound is based on multiparty communication complexity.
Back to Sam Buss's publications page.