Atserias, Kolaitis, and Vardi [AKV04] showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD( , weakening), simulates CP* (Cutting Planes with unary coefficients). We show that OBDD( , weakening) can give exponentially shorter proofs than dag-like cutting planes. This is proved by showing that the Clique-Coloring tautologies have polynomial size proofs in the OBDD( , weakening) system.

The reordering rule allows changing the variable order for OBDDs. We show that OBDD( , weakening, reordering) is strictly stronger than OBDD( , weakening). This is proved using the Clique-Coloring tautologies, and by transforming tautologies using coded permutations and orification. We also give CNF formulas which have polynomial size OBDD( ) proofs but require superpolynomial (actually, quasipolynomial size) resolution proofs, and thus we partially resolved open question proposed by Groote and Zantema [GZ03].

Applying dag-like and tree-like lifting techniques to the mentioned results we completely investigate the mutual strength for every pair of systems among C P , OBDD( ), OBDD( , weakening) and OBDD( , weakening, reordering). For dag-like proof systems, some of our separations are quasipolynomial and some are exponential; for tree-like systems, all of our separations are exponential.