Document Open Access Logo

Reordering Rule Makes OBDD Proof Systems Stronger

Authors Sam Buss, Dmitry Itsykson, Alexander Knop, Dmitry Sokolov

PDF
Thumbnail PDF

File

LIPIcs.CCC.2018.16.pdf
  • Filesize: 0.54 MB
  • 24 pages

Document Identifiers

Author Details

Sam Buss
  • University of California, San Diego, La Jolla, CA, USA
Dmitry Itsykson
  • St. Petersburg Department of V.A. Steklov Institute of Mathematics of the Russian Academy of Sciences, St. Petersburg, Russia
Alexander Knop
  • University of California, San Diego, La Jolla, CA, USA, St. Petersburg Department of V.A. Steklov Institute of Mathematics of the Russian Academy of Sciences, St. Petersburg, Russia
Dmitry Sokolov
  • KTH Royal Institute of Technology, Stockholm, Sweden , St. Petersburg Department of V.A. Steklov Institute of Mathematics of the Russian Academy of Sciences, St. Petersburg, Russia

Funding

The research was supported by the Russian Science Foundation (project 16-11-10123)

Cite AsGet BibTex

Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering Rule Makes OBDD Proof Systems Stronger. In 33rd Computational Complexity Conference (CCC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 102, pp. 16:1-16:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CCC.2018.16

Abstract

Atserias, Kolaitis, and Vardi showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD(^, weakening), simulates CP^* (Cutting Planes with unary coefficients). We show that OBDD(^, weakening) can give exponentially shorter proofs than dag-like cutting planes. This is proved by showing that the Clique-Coloring tautologies have polynomial size proofs in the OBDD(^, weakening) system. The reordering rule allows changing the variable order for OBDDs. We show that OBDD(^, weakening, reordering) is strictly stronger than OBDD(^, weakening). This is proved using the Clique-Coloring tautologies, and by transforming tautologies using coded permutations and orification. We also give CNF formulas which have polynomial size OBDD(^) proofs but require superpolynomial (actually, quasipolynomial size) resolution proofs, and thus we partially resolve an open question proposed by Groote and Zantema. Applying dag-like and tree-like lifting techniques to the mentioned results, we completely analyze which of the systems among CP^*, OBDD(^), OBDD(^, reordering), OBDD(^, weakening) and OBDD(^, weakening, reordering) polynomially simulate each other. For dag-like proof systems, some of our separations are quasipolynomial and some are exponential; for tree-like systems, all of our separations are exponential.

Subject Classification

ACM Subject Classification
  • Theory of computation → Computational complexity and cryptography
Keywords
  • Proof complexity
  • OBDD
  • Tseitin formulas
  • the Clique-Coloring principle
  • lifting theorems

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. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. URL: http://dx.doi.org/10.1145/375827.375835.
  3. Randal E. Bryant. Symbolic manipulation of boolean functions using a graphical representation. In Hillel Ofek and Lawrence A. O'Neill, editors, Proceedings of the 22nd ACM/IEEE conference on Design automation, DAC 1985, Las Vegas, Nevada, USA, 1985., pages 688-694. ACM, 1985. URL: http://dx.doi.org/10.1145/317825.317964.
  4. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 10\^20 states and beyond. Inf. Comput., 98(2):142-170, 1992. URL: http://dx.doi.org/10.1016/0890-5401(92)90017-A.
  5. Joshua Buresh-Oppenheim and Toniann Pitassi. The complexity of resolution refinements. J. Symb. Log., 72(4):1336-1352, 2007. URL: http://dx.doi.org/10.2178/jsl/1203350790.
  6. Wei Chen and Wenhui Zhang. A direct construction of polynomial-size OBDD proof of pigeon hole problem. Inf. Process. Lett., 109(10):472-477, 2009. URL: http://dx.doi.org/10.1016/j.ipl.2009.01.006.
  7. Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. Electronic Colloquium on Computational Complexity (ECCC), 24:175, 2017. URL: https://eccc.weizmann.ac.il/report/2017/175.
  8. Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. In David B. Shmoys, editor, Symposium on Theory of Computing, STOC 2014, New York, NY, USA, May 31 - June 03, 2014, pages 847-856. ACM, 2014. URL: http://dx.doi.org/10.1145/2591796.2591838.
  9. Dima Grigoriev, Edward A. Hirsch, and Dmitrii V. Pasechnik. Complexity of semi-algebraic proofs. In Helmut Alt and Afonso Ferreira, editors, STACS 2002, 19th Annual Symposium on Theoretical Aspects of Computer Science, Antibes - Juan les Pins, France, March 14-16, 2002, Proceedings, volume 2285 of Lecture Notes in Computer Science, pages 419-430. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-45841-7_34.
  10. 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.
  11. Dmitry Itsykson, Alexander Knop, Andrei E. Romashchenko, and Dmitry Sokolov. On obdd-based algorithms and proof systems that dynamically change order of variables. In Heribert Vollmer and Brigitte Vallée, editors, 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017, March 8-11, 2017, Hannover, Germany, volume 66 of LIPIcs, pages 43:1-43:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2017.43.
  12. Matti Järvisalo. On the relative efficiency of DPLL and obdds with axiom and join. In Jimmy Ho-Man Lee, editor, Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, volume 6876 of Lecture Notes in Computer Science, pages 429-437. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-23786-7_33.
  13. Jan Krajícek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log., 62(2):457-486, 1997. URL: http://dx.doi.org/10.2307/2275541.
  14. Jan Krajícek. An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams. J. Symb. Log., 73(1):227-237, 2008. URL: http://dx.doi.org/10.2178/jsl/1208358751.
  15. Kenneth L. McMillan. Symbolic model checking. Kluwer, 1993. Google Scholar
  16. Christoph Meinel and Anna Slobodova. On the complexity of constructing optimal ordered binary decision diagrams. In Proceedings of Mathematical Foundations of Computer Science, volume 841, pages 515-524, 1994. Google Scholar
  17. Guoqiang Pan and Moshe Y. Vardi. Search vs. symbolic techniques in satisfiability solving. In 7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, Revised Selected Papers, volume 3542, pages 235-250, 2005. URL: http://dx.doi.org/10.1007/11527695_19.
  18. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic, 62(3):981-998, 1997. Google Scholar
  19. 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. IEEE Computer Society, 2008. URL: http://dx.doi.org/10.1109/CCC.2008.34.
  20. Dmitry Sokolov. Dag-like communication and its applications. In Pascal Weil, editor, Computer Science - Theory and Applications - 12th International Computer Science Symposium in Russia, CSR 2017, Kazan, Russia, June 8-12, 2017, Proceedings, volume 10304 of Lecture Notes in Computer Science, pages 294-307. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-58747-9_26.
  21. Olga Tveretina, Carsten Sinz, and Hans Zantema. Ordered binary decision diagrams, pigeonhole formulas and beyond. JSAT, 7(1):35-58, 2010. URL: http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_3_Tveretina.pdf.
  22. Tomás E. Uribe and Mark E. Stickel. Ordered binary decision diagrams and the davis-putnam procedure. In Jean-Pierre Jouannaud, editor, Constraints in Computational Logics, First International Conference, CCL'94, Munich, Germant, September 7-9, 1994, volume 845 of Lecture Notes in Computer Science, pages 34-49. Springer, 1994. URL: http://dx.doi.org/10.1007/BFb0016843.
  23. Alasdair Urquhart. Hard examples for resolution. J. ACM, 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact