Результаты исследований: Материалы конференций › материалы › Рецензирование
OBDD(Join) Proofs Cannot Be Balanced. / Ovcharov, Sergei.
2023. 72:1-72:13 Работа представлена на 48th International Symposium on Mathematical Foundations of Computer Science, Bordeaux, Франция.Результаты исследований: Материалы конференций › материалы › Рецензирование
}
TY - CONF
T1 - OBDD(Join) Proofs Cannot Be Balanced.
AU - Ovcharov, Sergei
N1 - Conference code: 48
PY - 2023/8/21
Y1 - 2023/8/21
N2 - 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 Fn such that Fn has a polynomial-size tree-like OBDD(∧) refutation of depth poly(n) and for arbitrary OBDD(∧, reordering) refutation Π of Fn for every α ∈ (0, 1) the following trade-off holds: either the size of Π is 2Ω(nα) or the depth of Π is Ω(n1−α). As a corollary of the trade-offs, we get that OBDD(∧) and OBDD(∧, reordering) proofs cannot be balanced.
AB - 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 Fn such that Fn has a polynomial-size tree-like OBDD(∧) refutation of depth poly(n) and for arbitrary OBDD(∧, reordering) refutation Π of Fn for every α ∈ (0, 1) the following trade-off holds: either the size of Π is 2Ω(nα) or the depth of Π is Ω(n1−α). As a corollary of the trade-offs, we get that OBDD(∧) and OBDD(∧, reordering) proofs cannot be balanced.
KW - OBDD
KW - Proof complexity
KW - depth of proofs
KW - lower bounds
UR - https://www.mendeley.com/catalogue/55e3b55b-4dbf-331a-956b-0313180aa4a6/
U2 - 10.4230/LIPICS.MFCS.2023.72
DO - 10.4230/LIPICS.MFCS.2023.72
M3 - Paper
SP - 72:1-72:13
T2 - 48th International Symposium on Mathematical Foundations of Computer Science
Y2 - 28 August 2023 through 1 September 2023
ER -
ID: 108517146