Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
Reordering rule makes OBDD proof systems stronger. / Buss, Sam; Itsykson, Dmitry; Knop, Alexander; Sokolov, Dmitry.
33rd Computational Complexity Conference, CCC 2018. ed. / Rocco A. Servedio. Dagstuhl Publishing, 2018. p. 161-1624 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 102).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
}
TY - GEN
T1 - Reordering rule makes OBDD proof systems stronger
AU - Buss, Sam
AU - Itsykson, Dmitry
AU - Knop, Alexander
AU - Sokolov, Dmitry
PY - 2018/6/1
Y1 - 2018/6/1
N2 - 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.
AB - 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.
KW - Lifting theorems
KW - OBDD
KW - Proof complexity
KW - The Clique-Coloring principle
KW - Tseitin formulas
UR - http://www.scopus.com/inward/record.url?scp=85048982223&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CCC.2018.16
DO - 10.4230/LIPIcs.CCC.2018.16
M3 - Conference contribution
AN - SCOPUS:85048982223
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 161
EP - 1624
BT - 33rd Computational Complexity Conference, CCC 2018
A2 - Servedio, Rocco A.
PB - Dagstuhl Publishing
T2 - 33rd Computational Complexity Conference, CCC 2018
Y2 - 22 June 2018 through 24 June 2018
ER -
ID: 49785215