Document Open Access Logo

On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables

Authors Dmitry Itsykson, Alexander Knop, Andrey Romashchenko, Dmitry Sokolov

PDF
Thumbnail PDF

File

LIPIcs.STACS.2017.43.pdf
  • Filesize: 0.49 MB
  • 14 pages

Document Identifiers

Author Details

Dmitry Itsykson
Alexander Knop
Andrey Romashchenko
Dmitry Sokolov

Cite As Get BibTex

Dmitry Itsykson, Alexander Knop, Andrey Romashchenko, and Dmitry Sokolov. On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 43:1-43:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.STACS.2017.43

Abstract

In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of identically false OBDD from OBDDs representing clauses of the initial formula. All OBDDs in such proofs have the same order of variables. We initiate the study of OBDD based proof systems that additionally contain a rule that allows to change the order in OBDDs. At first we consider a proof system OBDD(and, reordering) that uses the conjunction (join) rule and the rule that allows to change the order. We exponentially separate this proof system from OBDD(and)-proof system that uses only the conjunction rule. We prove two exponential lower bounds on the size of OBDD(and, reordering)-refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for OBDD(and)-proofs and the second one extends the result of Tveretina et al. from OBDD(and) to OBDD(and, reordering).

In 2004 Pan and Vardi proposed an approach to the propositional satisfiability problem based on OBDDs and symbolic quantifier elimination (we denote algorithms based on this approach as OBDD(and, exists)-algorithms. We notice that there exists an OBDD(and, exists)-algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time. In contrast, we show that there exist formulas representing systems of linear equations over F_2 that are hard for OBDD(and, exists, reordering)-algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over F_2 that correspond to some checksum matrices of error correcting codes.

Subject Classification

Keywords
  • Proof complexity
  • OBDD
  • error-correcting codes
  • Tseitin formulas
  • expanders

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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, volume 3258 of Lecture Notes in Computer Science, pages 77-91. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30201-8_9.
  2. Paul Beame, Toniann Pitassi, and Nathan Segerlind. Lower Bounds for Lovász-Schrijver Systems and Beyond Follow from Multiparty Communication Complexity. SIAM J. Comput., 37(3):845-869, 2007. URL: http://dx.doi.org/10.1137/060654645.
  3. Randal E. Bryant. Symbolic manipulation of boolean functions using a graphical representation. In Proceedings of the 22nd ACM/IEEE conference on Design automation, DAC 1985, Las Vegas, Nevada, USA, 1985., pages 688-694, 1985. URL: http://dx.doi.org/10.1145/317825.317964.
  4. Wěi Chén and Wenhui Zhang. A direct construction of polynomial-size OBDD proof of pigeon hole problem. Information Processing Letters, 109(10):472-477, 2009. URL: http://dx.doi.org/10.1016/j.ipl.2009.01.006.
  5. Pavol Duris, Juraj Hromkovic, Stasys Jukna, Martin Sauerhoff, and Georg Schnitger. On multi-partition communication complexity. Inf. Comput., 194(1):49-75, 2004. URL: http://dx.doi.org/10.1016/j.ic.2004.05.002.
  6. Luke Friedman and Yixin Xu. Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams. In Andrei A. Bulatov and Arseny M. Shur, editors, CSR 2013, volume 7913 of Lecture Notes in Computer Science, pages 127-138. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-38536-0_11.
  7. Robert G. Gallager. Low-density parity-check codes. Information Theory, IRE Transactions on, 8(1):21-28, 1962. Google Scholar
  8. Jan Friso Groote and Hans Zantema. Resolution and binary decision diagrams cannot simulate each other polynomially. Discrete Applied Mathematics, 130(2):157-171, 2003. URL: http://dx.doi.org/10.1016/S0166-218X(02)00403-1.
  9. Venkatesan Guruswami. List decoding from erasures: bounds and code constructions. Information Theory, IEEE Transactions on, 49(11):2826-2833, 2003. URL: http://dx.doi.org/10.1109/tit.2003.815776.
  10. Jan Krajíček. An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams. Journal of Symbolic Logic, 73(1):227-237, 2008. URL: http://dx.doi.org/10.2178/jsl/1208358751.
  11. Eyal Kushilevitz and Noam Nisan. Communication complexity. Cambridge University Press, 1997. Google Scholar
  12. A. Lubotzky, R. Phillips, and P. Sarnak. Ramanujan graphs. Combinatorica, 8(3):261-277, 1988. Google Scholar
  13. Christoph Meinel and Anna Slobodova. On the complexity of Constructing Optimal Ordered Binary Decision Diagrams. Proceedings of Mathematical Foundations of Computer Science, 841:515-524, 1994. Google Scholar
  14. Christoph Meinel and Thorsten Theobald. Algorithms and Data Structures in VLSI Design: OBDD - Foundations and Applications. Springer, 1998. Google Scholar
  15. Guoqiang Pan and Moshe Y. Vardi. Search vs. Symbolic Techniques in Satisfiability Solving. 7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, Revised Selected Papers, 3542:235-250, 2005. URL: http://dx.doi.org/10.1007/11527695_19.
  16. Nathan Segerlind. Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability. CoRR, abs/cs/070:40, 2007. URL: http://arxiv.org/abs/0701054.
  17. Nathan Segerlind. On the relative efficiency of resolution-like proofs and ordered binary decision diagram proofs. In Proceedings of the 23rd Annual IEEE Conference on Computational Complexity, CCC 2008, 23-26 June 2008, College Park, Maryland, USA, pages 100-111, 2008. URL: http://dx.doi.org/10.1109/CCC.2008.34.
  18. Olga Tveretina, Carsten Sinz, and Hans Zantema. An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas. Proceedings Fourth Athens Colloquium on Algorithms and Complexity, 4(Acac):13-21, 2009. http://arxiv.org/abs/0909.5038, URL: http://dx.doi.org/10.4204/EPTCS.4.2.
  19. Alasdair Urquhart. Hard Examples for Resolution. JACM, 34(1):209-219, 1987. URL: http://dx.doi.org/10.1145/7531.8928.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact