A propositional proof system based on ordered binary decision diagrams (OBDDs) was introduced by Atserias et al. Krajicek proved exponential lower bounds for a strong variant of this system using feasible interpolation, and Tveretina et al. proved exponential lower bounds for restricted versions of this system for refuting formulas derived from the Pigeonhole Principle.
In this paper we prove the first lower bounds for refuting randomly generated unsatisfiable formulas in restricted versions of this OBDD-based proof system.
In particular we consider two systems OBDD* and OBDD+; OBDD* is restricted by having a fixed, predetermined variable order for all OBDDs in its refutations, and OBDD+ is restricted by having a fixed order in which the clauses of the input formula must be processed.
We show that for some constant $\epsilon > 0$, with high probability an OBDD* refutation of an unsatisfiable random 3-CNF formula must be of size at least $2^{\epsilon n}$, and an OBDD+ refutation of an unsatisfiable random 3-XOR formula must be of size at least $2^{\epsilon n}$.