Sam Buss, Alexander Knop,
Dmitry Itsykson, and Dmitry Sokolov
Reordering Rule Makes OBDD Proof Systems Stronger
Preprint, January 2018.
Abstract: Atserias, Kolaitis, and Vardi showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD(and,weakening), simulates CP* (Cutting Planes with unary coefficients). We show that OBDD(and,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(and,weakening) system. The reordering rule allows changing the variable order for OBDDs. We show that OBDD(and,weakening,reordering) is strictly stronger than OBDD(and,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(and) proofs but require superpolynomial (actually, quasipolynomial size) resolution proofs, and thus we partially resolved open question proposed by Groote and Zantema. Applying dag-like and tree-like lifting techniques to the mentioned results we completely investigate the mutual strength for every pair of systems among CP*, OBDD(and), OBDD(and,weakening), OBDD(and,weakening) and OBDD(and,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.
Back to Sam Buss's publications page.