ABSTRACT. It is well-known that there is an equivalence between ordered resolution and ordered binary decision diagrams (OBDD); i.e., for any unsatisfiable formula phi, the size of the smallest ordered resolution refutation of phi equal to the size of the smallest OBDD for the canonical search problem corresponding to phi. But there is no such equivalence between resolution and branching programs (BP).

In this project, we study different proof systems equivalent to classes of branching programs between BP and OBDD. These proof systems are similar to roABP-IPS, an algebraic proof system defined by Forbes et al. and based on the ideal proof system introduced by Grochow and Pitassi.

We show that proof systems equivalent to b-OBDD are not comparable with resolution and cutting planes (for b > 1). We also prove exponential lower bounds for these proof systems on Tseitin formulas. Additionally, we show that proof systems equivalent to (1,+b)-BP are strictly stronger than regular resolution for b > 0; moreover, resolution does not p-simulate (1, +b)-BP for b > 5.