This article 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
n
vertices and an ε > 0, such that 1-NBP(∧, ∃
ε
n
) refutations of the Tseitin formula for
G
n
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.
Correction to: Near-Optimal Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs
