Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Paper:

TR18-041 | 26th February 2018 20:46

#### Reordering Rule Makes OBDD Proof Systems Stronger

TR18-041
Authors: Sam Buss, Dmitry Itsykson, Alexander Knop, Dmitry Sokolov
Publication: 26th February 2018 20:52
Keywords:

Abstract:

Atserias, Kolaitis, and Vardi [AKV04] showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD(\$\land\$, weakening), simulates CP* (Cutting Planes with unary coefficients). We show that OBDD(\$\land\$, 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(\$\land\$, weakening) system.

The reordering rule allows changing the variable order for OBDDs. We show that OBDD(\$\land\$, weakening, reordering) is strictly stronger than OBDD(\$\land\$, 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(\$\land\$) 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 \$CP^*\$, OBDD(\$\land\$), OBDD(\$\land\$, weakening) and OBDD(\$\land\$, 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.

ISSN 1433-8092 | Imprint