Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Buss, Sam; Itsykson, Dmitry; Knop, Alexander; Sokolov, Dmitry http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-88720
URL:

; ; ;

Reordering Rule Makes OBDD Proof Systems Stronger

pdf-format:


Abstract

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.

BibTeX - Entry

@InProceedings{buss_et_al:LIPIcs:2018:8872,
  author =	{Sam Buss and Dmitry Itsykson and Alexander Knop and Dmitry Sokolov},
  title =	{{Reordering Rule Makes OBDD Proof Systems Stronger}},
  booktitle =	{33rd Computational Complexity Conference (CCC 2018)},
  pages =	{16:1--16:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-069-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{102},
  editor =	{Rocco A. Servedio},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8872},
  URN =		{urn:nbn:de:0030-drops-88720},
  doi =		{10.4230/LIPIcs.CCC.2018.16},
  annote =	{Keywords: Proof complexity, OBDD, Tseitin formulas, the Clique-Coloring principle, lifting theorems}
}

Keywords: Proof complexity, OBDD, Tseitin formulas, the Clique-Coloring principle, lifting theorems
Seminar: 33rd Computational Complexity Conference (CCC 2018)
Issue date: 2018
Date of publication: 2018


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI