Document Open Access Logo

Automating OBDD proofs is NP-hard

Authors Dmitry Itsykson , Artur Riazanov

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.59.pdf
  • Filesize: 0.81 MB
  • 15 pages

Document Identifiers

Author Details

Dmitry Itsykson
  • Steklov Institute of Mathematics at St. Petersburg, Russia
Artur Riazanov
  • Steklov Institute of Mathematics at St. Petersburg, Russia

Funding

The research is supported by Russian Science Foundation (project 18-71-10042).

Acknowledgements

The authors thank Anastasia Sofronova and Michal Garl´ık for fruitful discussions, Anastasia Sofronova for her comments on the draft. They also thank anonymous referees for their feedback. Artur Riazanov additionally thanks Dmitry Sokolov for his patient explanations of the lifting technique in [Garg et al., 2018].

Cite AsGet BibTex

Dmitry Itsykson and Artur Riazanov. Automating OBDD proofs is NP-hard. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 59:1-59:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.59

Abstract

We prove that the proof system OBDD(∧, weakening) is not automatable unless P = NP. The proof is based upon the celebrated result of [Albert Atserias and Moritz Müller, 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with multi-output indexing gadget from resolution block-width to dag-like multiparty number-in-hand communication protocol size with o(n) parties, where n is the number of variables in the non-lifted formula. A similar lifting theorem for protocols with n+1 participants was proved by [Göös et al., 2020] to establish the hardness of automatability result for Cutting Planes.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • OBDD
  • automatability
  • lifting
  • dag-like communication

Metrics

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

Related Versions

References

  1. Alfonso San Miguel Aguirre and Moshe Y. Vardi. Random 3-sat and bdds: The plot thickens further. In Principles and Practice of Constraint Programming - CP 2001, 7th International Conference, CP 2001, Paphos, Cyprus, November 26 - December 1, 2001, Proceedings, pages 121-136, 2001. URL: https://doi.org/10.1007/3-540-45578-7_9.
  2. Michael Alekhnovich, Samuel R. Buss, Shlomo Moran, and Toniann Pitassi. Minimum propositional proof length is np-hard to linearly approximate. J. Symb. Log., 66(1):171-191, 2001. URL: https://doi.org/10.2307/2694916.
  3. Michael Alekhnovich and Alexander A. Razborov. Resolution is not automatizable unless W[P] is tractable. SIAM J. Comput., 38(4):1347-1363, 2008. URL: https://doi.org/10.1137/06066850X.
  4. 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.
  5. Albert Atserias and Moritz Müller. Automating resolution is np-hard. In David Zuckerman, editor, 60th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2019, Baltimore, Maryland, USA, November 9-12, 2019, pages 498-509. IEEE Computer Society, 2019. URL: https://doi.org/10.1109/FOCS.2019.00038.
  6. Maria Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, and Toniann Pitassi. Non-automatizability of bounded-depth frege proofs. Comput. Complex., 13(1-2):47-68, 2004. URL: https://doi.org/10.1007/s00037-004-0183-5.
  7. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. No feasible interpolation for tc0-frege proofs. In 38th Annual Symposium on Foundations of Computer Science, FOCS '97, Miami Beach, Florida, USA, October 19-22, 1997, pages 254-263. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/SFCS.1997.646114.
  8. Randal E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagram. ACM Computing Surveys, 24(3):293-318, 1992. Google Scholar
  9. Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering rule makes OBDD proof systems stronger. In 33rd Computational Complexity Conference, CCC 2018, June 22-24, 2018, San Diego, CA, USA, pages 16:1-16:24, 2018. URL: https://doi.org/10.4230/LIPIcs.CCC.2018.16.
  10. Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, page 902–911, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3188745.3188838.
  11. Michal Garlík. Failure of feasible disjunction property for k-dnf resolution and np-hardness of automating it. Electron. Colloquium Comput. Complex., page 37, 2020. URL: https://eccc.weizmann.ac.il/report/2020/037.
  12. Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating cutting planes is np-hard. In Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, pages 68-77, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3357713.3384248.
  13. Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, Dmitry Sokolov, and Susanna F. de Rezende. Automating algebraic proof systems is np-hard. Electron. Colloquium Comput. Complex., 27:64, 2020. URL: https://eccc.weizmann.ac.il/report/2020/064.
  14. 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.
  15. Kazuo Iwama. Complexity of finding short resolution proofs. In Igor Prívara and Peter Ruzicka, editors, Mathematical Foundations of Computer Science 1997, 22nd International Symposium, MFCS'97, Bratislava, Slovakia, August 25-29, 1997, Proceedings, volume 1295 of Lecture Notes in Computer Science, pages 309-318. Springer, 1997. URL: https://doi.org/10.1007/BFb0029974.
  16. Jan Krajič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: https://doi.org/10.2178/jsl/1208358751.
  17. Jan Krajícek and Pavel Pudlák. Some consequences of cryptographical conjectures for s¹₂ and EF. Inf. Comput., 140(1):82-94, 1998. URL: https://doi.org/10.1006/inco.1997.2674.
  18. 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
  19. Ian Mertz, Toniann Pitassi, and Yuanhao Wei. Short proofs are hard to find. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, volume 132 of LIPIcs, pages 84:1-84:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.84.
  20. Guoqiang Pan and Moshe Y. Vardi. Symbolic techniques in satisfiability solving. Journal of Automated Reasoning, 35(1-3):25-50, 2005. URL: https://doi.org/10.1007/s10817-005-9009-7.
  21. Jeff M. Phillips, Elad Verbin, and Qin Zhang. Lower bounds for number-in-hand multiparty communication complexity, made easy. In Proceedings of the Twenty-Third Annual ACM-SIAM Symposium on Discrete Algorithms, SODA '12, pages 486-501, USA, 2012. Society for Industrial and Applied Mathematics. Google Scholar
  22. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log., 62(3):981-998, 1997. URL: https://doi.org/10.2307/2275583.
  23. Nathan Segerlind. Nearly-exponential size lower bounds for symbolic quantifier elimination algorithms and OBDD-based proofs of unsatisfiability. Electronic Colloquium on Computational Complexity (ECCC), 14(009), 2007. URL: http://eccc.hpi-web.de/eccc-reports/2007/TR07-009/index.html.
  24. 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: https://doi.org/10.1109/CCC.2008.34.
  25. Dmitry Sokolov. Dag-like communication and its applications. In Computer Science - Theory and Applications - 12th International Computer Science Symposium in Russia, CSR 2017, Kazan, Russia, June 8-12, 2017, Proceedings, pages 294-307, 2017. URL: https://doi.org/10.1007/978-3-319-58747-9_26.
  26. I. Wegener. Branching Programs and Binary Decision Diagrams: Theory and Applications. Discrete Mathematics and Applications. Society for Industrial and Applied Mathematics, 2000. URL: https://books.google.ru/books?id=xqqJj42ZoXcC.
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 Imprint Privacy Contact