OBDD(Join) Proofs Cannot Be Balanced

Ovcharov, Sergei

doi:10.4230/LIPIcs.MFCS.2023.72

File

LIPIcs.MFCS.2023.72.pdf

Filesize: 0.73 MB
13 pages

Document Identifiers

DOI: 10.4230/LIPIcs.MFCS.2023.72
URN: urn:nbn:de:0030-drops-186065

Author Details

Sergei Ovcharov

St. Petersburg State University, Russia

Acknowledgements

The author is grateful to his supervisor Dmitry Itsykson for a suggesting of the problem, for the many fruitful discussions of it and for his active help in the preparation of this paper.

Cite AsGet BibTex

Sergei Ovcharov. OBDD(Join) Proofs Cannot Be Balanced. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 72:1-72:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.MFCS.2023.72

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.

Subject Classification

ACM Subject Classification

Theory of computation → Proof complexity

Keywords

Proof complexity
OBDD
lower bounds
depth of proofs

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

Albert Atserias, Maria Luisa Bonet, and Jordi Levy. On Chvatal rank and cutting planes proofs. Electron. Colloquium Comput. Complex., TR03-041, 2003. URL: https://arxiv.org/abs/TR03-041.
Albert Atserias, Phokion G. Kolaitis, and Moshe Y. Vardi. Constraint propagation as a proof system. In Mark Wallace, editor, Principles and Practice of Constraint Programming - CP 2004, 10th International Conference, CP 2004, Toronto, Canada, September 27 - October 1, 2004, Proceedings, volume 3258 of Lecture Notes in Computer Science, pages 77-91. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30201-8_9.
Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res., 22:319-351, 2004. URL: https://doi.org/10.1613/jair.1410.
Eli Ben-Sasson and Jakob Nordström. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Bernard Chazelle, editor, Innovations in Computer Science - ICS 2011, Tsinghua University, Beijing, China, January 7-9, 2011. Proceedings, pages 401-416. Tsinghua University Press, 2011. URL: http://conference.iiis.tsinghua.edu.cn/ICS2011/content/papers/3.html.
Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow—resolution made simple. J. ACM, 48(2):149-169, March 2001. URL: https://doi.org/10.1145/375827.375835.
Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986. URL: https://doi.org/10.1109/TC.1986.1676819.
Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering rule makes OBDD proof systems stronger. Electron. Colloquium Comput. Complex., TR18-041, 2018. URL: https://arxiv.org/abs/TR18-041.
Donald Chai and Andreas Kuehlmann. A fast pseudo-boolean constraint solver. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 24(3):305-317, 2005. URL: https://doi.org/10.1109/TCAD.2004.842808.
Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
William J. Cook, Collette R. Coullard, and György Turán. On the complexity of cutting-plane proofs. Discret. Appl. Math., 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
Shlomo Hoory, Nathan Linial, and Avi Wigderson. Expander graphs and their applications. Bull. Amer. Math. Soc., 43(04):439-562, August 2006. URL: https://doi.org/10.1090/s0273-0979-06-01126-8.
Dmitry Itsykson, Alexander Knop, Andrei E. Romashchenko, and Dmitry Sokolov. On obdd-based algorithms and proof systems that dynamically change the order of variables. J. Symb. Log., 85(2):632-670, 2020. URL: https://doi.org/10.1017/jsl.2019.53.
Christoph Meinel and Anna Slobodová. On the complexity of constructing optimal ordered binary decision diagrams. In Igor Prívara, Branislav Rovan, and Peter Ruzicka, editors, Mathematical Foundations of Computer Science 1994, 19th International Symposium, MFCS'94, Kosice, Slovakia, August 22-26, 1994, Proceedings, volume 841 of Lecture Notes in Computer Science, pages 515-524. Springer, 1994. URL: https://doi.org/10.1007/3-540-58338-6_98.
Christoph Meinel and Thorsten Theobald. Algorithms and Data Structures in VLSI Design: OBDD - Foundations and Applications. Springer, 1998. URL: http://www.informatik.uni-trier.de/%7Emeinel/books/obddbook.html.
Pavel Pudlák and Samuel R. Buss. How to lie without being (easily) convicted and the length of proofs in propositional calculus. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 151-162. Springer, 1994. URL: https://doi.org/10.1007/BFb0022253.
Alasdair Urquhart. The depth of resolution proofs. Stud Logica, 99(1-3):349-364, 2011. URL: https://doi.org/10.1007/s11225-011-9356-9.