Abstract
We study OBDDbased 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 polynomialsize increase. We construct a family of unsatisfiable CNF formulas F_n such that F_n has a polynomialsize treelike OBDD(∧) refutation of depth poly(n) and for arbitrary OBDD(∧, reordering) refutation Π of F_n for every α ∈ (0,1) the following tradeoff holds: either the size of Π is 2^Ω(n^α) or the depth of Π is Ω(n^{1α}). As a corollary of the tradeoffs, 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:172:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772921},
ISSN = {18688969},
year = {2023},
volume = {272},
editor = {Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18606},
URN = {urn:nbn:de:0030drops186065},
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 