License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CCC.2018.16
URN: urn:nbn:de:0030-drops-88720
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8872/
Go to the corresponding LIPIcs Volume Portal

Buss, Sam ; Itsykson, Dmitry ; Knop, Alexander ; Sokolov, Dmitry

Reordering Rule Makes OBDD Proof Systems Stronger

pdf-format:
LIPIcs-CCC-2018-16.pdf (0.5 MB)

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 f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://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
Collection: 33rd Computational Complexity Conference (CCC 2018)
Issue Date: 2018
Date of publication: 04.06.2018

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