Name
Abstract | ||
|---|---|---|
Atserias, Kolaitis, and Vardi showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD(Lambda, weakening), simulates CP (Cutting Planes with unary coefficients). We show that OBDD(Lambda 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(Lambda, weakening) system. The reordering rule allows changing the variable order for OBDDs. We show that OBDD(Lambda, weakening, reordering) is strictly stronger than OBDD(Lambda, 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(Lambda) 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(Lambda), OBDD(Lambda, reordering), OBDD(Lambda, weakening) and OBDD(Lambda, 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. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.4230/LIPIcs.CCC.2018.16 | Leibniz International Proceedings in Informatics |
Keywords | DocType | Volume |
Proof complexity,OBDD,Tseitin formulas,the Clique-Coloring principle,lifting theorems | Conference | 102 |
ISSN | Citations | PageRank |
1868-8969 | 0 | 0.34 |
References | Authors | |
0 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Samuel R. Buss | 1 | 956 | 84.19 |
| Dmitry Itsykson | 2 | 33 | 10.09 |
| Alexander Knop | 3 | 3 | 5.69 |
| Dmitry Sokolov | 4 | 12 | 4.76 |