ECCC-Report TR20-073https://eccc.weizmann.ac.il/report/2020/073Comments and Revisions published for TR20-073en-usTue, 05 May 2020 21:13:59 +0300
Paper TR20-073
| Lower Bounds on OBDD Proofs with Several Orders |
Dmitry Itsykson,
Sam Buss,
Dmitry Sokolov,
Alexander Knop,
Artur Riazanov
https://eccc.weizmann.ac.il/report/2020/073This paper is motivated by seeking lower bounds on OBDD($\land$, weakening, reordering) refutations, namely OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1-NBP($\land$) refutations based on read-once nondeterministic branching programs. These generalize OBDD($\land$, reordering) refutations. There are polynomial size 1-NBP($\land$) refutations of the pigeonhole principle, hence 1-NBP($\land$) is strictly stronger than OBDD($\land$, reordering). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP($\land$) refutations. As a corollary, OBDD($\land$, reordering) does not simulate tree-like resolution, answering a previously open question.
The system 1-NBP($\land$, $\exists$) uses projection inferences instead of weakening. 1-NBP($\land$, $\exists_k$) is the system restricted to projection on at most $k$ distinct variables. We construct explicit constant degree graphs $G_n$ on $n$ vertices and an $\epsilon > 0$, such that 1-NBP($\land$, $\exists_{\epsilon n}$) refutations of the Tseitin formula for $G_n$ require exponential size.
Second, we study the proof system OBDD($\land$, weakening, reordering$_\ell$) which allows $\ell$ different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD($\land$, weakening, reordering$_\ell$) refutations for $\ell = \epsilon \log n$, where $n$ is the number of variables and $\epsilon > 0$ is a constant. The lower bound is based on multiparty communication complexity.Tue, 05 May 2020 21:13:59 +0300https://eccc.weizmann.ac.il/report/2020/073