2026-07-24T01:45:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8872 2024-03-06T10:42:52Z ddc:004 open_access

Reordering Rule Makes OBDD Proof Systems Stronger Buss, Sam Itsykson, Dmitry Knop, Alexander Sokolov, Dmitry Proof complexity OBDD Tseitin formulas the Clique-Coloring principle lifting theorems Atserias, Kolaitis, and Vardi 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 resolve an open question proposed by Groote and Zantema. Applying dag-like and tree-like lifting techniques to the mentioned results, we completely analyze which of the systems among CP^*, OBDD(^), OBDD(^, reordering), OBDD(^, weakening) and OBDD(^, weakening, reordering) polynomially simulate each other. 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sam Buss and Dmitry Itsykson and Alexander Knop and Dmitry Sokolov 2018 Is Part Of LIPIcs, Volume 102, 33rd Computational Complexity Conference (CCC 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CCC.2018.16 urn:nbn:de:0030-drops-88720 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2018.16 eng https://creativecommons.org/licenses/by/3.0/legalcode