__Preprint:__

**
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.
**

**
Download
preprint.
**

**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 *G _{n}*
on