Standard

OBDD(Join) Proofs Cannot Be Balanced. / Ovcharov, Sergei.

2023. 72:1-72:13 Paper presented at 48th International Symposium on Mathematical Foundations of Computer Science, Bordeaux, France.

Research output: Contribution to conference › Paper › peer-review

Harvard

Ovcharov, S 2023, 'OBDD(Join) Proofs Cannot Be Balanced.', Paper presented at 48th International Symposium on Mathematical Foundations of Computer Science, Bordeaux, France, 28/08/23 - 1/09/23 pp. 72:1-72:13. https://doi.org/10.4230/LIPICS.MFCS.2023.72

APA

Ovcharov, S. (2023). OBDD(Join) Proofs Cannot Be Balanced.. 72:1-72:13. Paper presented at 48th International Symposium on Mathematical Foundations of Computer Science, Bordeaux, France. https://doi.org/10.4230/LIPICS.MFCS.2023.72

Vancouver

Ovcharov S. OBDD(Join) Proofs Cannot Be Balanced.. 2023. Paper presented at 48th International Symposium on Mathematical Foundations of Computer Science, Bordeaux, France. https://doi.org/10.4230/LIPICS.MFCS.2023.72

Author

Ovcharov, Sergei. / OBDD(Join) Proofs Cannot Be Balanced. Paper presented at 48th International Symposium on Mathematical Foundations of Computer Science, Bordeaux, France.13 p.

BibTeX

@conference{f7d9aaef5c5b4b698c4eb58d3a1f9e22,
title = "OBDD(Join) Proofs Cannot Be Balanced.",
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 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.",
keywords = "OBDD, Proof complexity, depth of proofs, lower bounds",
author = "Sergei Ovcharov",
note = "DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.; 48th International Symposium on Mathematical Foundations of Computer Science ; Conference date: 28-08-2023 Through 01-09-2023",
year = "2023",
month = aug,
day = "21",
doi = "10.4230/LIPICS.MFCS.2023.72",
language = "English",
pages = "72:1--72:13",
url = "https://mfcs2023.labri.fr",

}

RIS

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