License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2023.72
URN: urn:nbn:de:0030-drops-186065
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18606/
Go to the corresponding LIPIcs Volume Portal

Ovcharov, Sergei

OBDD(Join) Proofs Cannot Be Balanced

pdf-format:
LIPIcs-MFCS-2023-72.pdf (0.7 MB)

Abstract

We study OBDD-based propositional proof systems introduced in 2004 by Atserias, Kolaitis, and Vardi that prove the unsatisfiability of a CNF formula by deduction of an identically false OBDD from OBDDs representing clauses of the initial formula. We consider a proof system OBDD(∧) that uses only the conjunction (join) rule and a proof system OBDD(∧, reordering) (introduced in 2017 by Itsykson, Knop, Romashchenko, and Sokolov) that uses the conjunction (join) rule and the rule that allows changing the order of variables in OBDD.
We study whether these systems can be balanced i.e. every refutation of size S can be reassembled into a refutation of depth O(log S) with at most a polynomial-size increase. We construct a family of unsatisfiable CNF formulas F_n such that F_n has a polynomial-size tree-like OBDD(∧) refutation of depth poly(n) and for arbitrary OBDD(∧, reordering) refutation Π of F_n for every α ∈ (0,1) the following trade-off holds: either the size of Π is 2^Ω(n^α) or the depth of Π is Ω(n^{1-α}). As a corollary of the trade-offs, we get that OBDD(∧) and OBDD(∧, reordering) proofs cannot be balanced.

BibTeX - Entry

@InProceedings{ovcharov:LIPIcs.MFCS.2023.72,
  author =	{Ovcharov, Sergei},
  title =	{{OBDD(Join) Proofs Cannot Be Balanced}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{72:1--72:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18606},
  URN =		{urn:nbn:de:0030-drops-186065},
  doi =		{10.4230/LIPIcs.MFCS.2023.72},
  annote =	{Keywords: Proof complexity, OBDD, lower bounds, depth of proofs}
}

Keywords: Proof complexity, OBDD, lower bounds, depth of proofs
Collection: 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)
Issue Date: 2023
Date of publication: 21.08.2023

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