2026-07-22T19:33:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18606 2024-03-06T11:02:15Z ddc:004 open_access

OBDD(Join) Proofs Cannot Be Balanced Ovcharov, Sergei Proof complexity OBDD lower bounds depth of proofs 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sergei Ovcharov 2023 Is Part Of LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2023.72 urn:nbn:de:0030-drops-186065 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.72 eng https://creativecommons.org/licenses/by/4.0/legalcode