Document Open Access Logo

Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs

Authors Sam Buss, Anupam Das, Alexander Knop

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.12.pdf
  • Filesize: 0.53 MB
  • 17 pages

Document Identifiers

Author Details

Sam Buss
  • Dept. of Mathematics, UC San Diego, USA
Anupam Das
  • Dept. of Computer Science, University of Copenhagen, Denmark
Alexander Knop
  • Dept. of Mathematics, UC San Diego, USA

Funding

  • Buss, Sam: This work supported in part by Simons Foundation grant 578919.
  • Das, Anupam: This work was supported by a Marie Skłodowska-Curie fellowship, Monotonicity in Logic and Complexity, ERC project 753431.

Cite AsGet BibTex

Sam Buss, Anupam Das, and Alexander Knop. Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CSL.2020.12

Abstract

This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs, deterministic or non-deterministic. Decision trees (DTs) are represented by a natural term syntax, inducing the system LDT, and non-determinism is modelled by including disjunction, ∨, as primitive (system LNDT). Branching programs generalise DTs to dag-like structures and are duly handled by extension variables in our setting, as is common in proof complexity (systems eLDT and eLNDT). Deterministic and non-deterministic branching programs are natural nonuniform analogues of log-space (L) and nondeterministic log-space (NL), respectively. Thus eLDT and eLNDT serve as natural systems of reasoning corresponding to L and NL, respectively. The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in LDT, LNDT, eLDT and eLNDT. We also compare them with Frege systems, constant-depth Frege systems and extended Frege systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Computational complexity and cryptography
Keywords
  • proof complexity
  • decision trees
  • branching programs
  • logspace
  • sequent calculus
  • non-determinism
  • low-depth complexity

Metrics

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

Related Versions

References

  1. Toshiyasu Arai. A Bounded Arithmetic AID for Frege Systems. Annals of Pure and Applied Logic, 103:155-199, 2000. Google Scholar
  2. Arnold Beckmann and Samuel R. Buss. Separation Results for the Size of Constant-Depth Propositional Proofs. Annals of Pure and Applied Logic, 136:30-55, 2005. Google Scholar
  3. Arnold Beckmann and Samuel R. Buss. On Transformations of Constant Depth Propositional Proofs. Annals of Pure and Applied Logic, ??:???-???, 2019. To appear. URL: https://doi.org/10.1016/j.apal.2019.05.002.
  4. Sam Buss. Quasipolynomial Size Proofs of the Propositional Pigeonhole Principle. Theoretical Computer Science, 576(C):77-84, 2015. URL: https://doi.org/10.1016/j.tcs.2015.02.005.
  5. Sam Buss, Anupam Das, and Alexander Knop. Proof complexity of systems of (non-deterministic) decision trees and branching programs, 2019. URL: http://arxiv.org/abs/1910.08503.
  6. 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.
  7. Samuel R. Buss. Bounded Arithmetic. Bibliopolis, Naples, Italy, 1986. Revision of 1985 Princeton University Ph.D. thesis. Google Scholar
  8. Samuel R. Buss. The Boolean Formula Value Problem is in ALOGTIME. In Proceedings of the 19-th Annual ACM Symposium on Theory of Computing, pages 123-131, May 1987. Google Scholar
  9. Samuel R. Buss and Pavel Pudlák. How to Lie Without Being (Easily) Convicted and the Lengths of Proofs in Propositional Calculus. In L. Pacholski and J. Tiuryn, editors, Proceedings of the 8th Workshop on Computer Science Logic, Kazimierz, Poland, September 1994, Lecture Notes in Computer Science #933, pages 151-162, Berlin, 1995. Springer-Verlag. Google Scholar
  10. Stephen A. Cook. A Survey of Complexity Classes and Their Associated Propositional Proof Systems and Theories, and a Proof System for Log Space. Talk presented at the ICMS Workshop on Circuit and Proof Complexity, Edinburgh, October 2001. http://www.cs.toronto.edu/ sacook/. Google Scholar
  11. Stephen A. Cook. Feasibly Constructive Proofs and the Propositional Calculus. In Proceedings of the Seventh Annual ACM Symposium on Theory of Computing, pages 83-97. Association for Computing Machinery, 1975. Google Scholar
  12. Stephen A. Cook and Antonina Kolokolova. A Second-Order System for Polytime Reasoning based on Grädel’s Theorem. Annals of Pure and Applied Logic, 124:193-231, 2003. Google Scholar
  13. Stephen A. Cook and Antonina Kolokolova. A Second-Order Theory for NL. In Proc. 19th IEEE Symp. on Logic in Computer Science (LICS'04), pages 398-407, 2004. Google Scholar
  14. Stephen A. Cook and Tsuyoshi Morioka. Quantified Propositional Calculus and A Second-Order Theory for NC¹. Archive for Mathematical Logic, 44:711-749, 2005. Google Scholar
  15. Stephen A. Cook and Phuong Nguyen. Foundations of Proof Complexity: Bounded Arithmetic and Propositional Translations. ASL and Cambridge University Press, 2010. 496 pages. Google Scholar
  16. Stephen A. Cook and Robert A. Reckhow. On the Lengths of Proofs in the Propositional Calculus, Preliminary Version. In Proceedings of the Sixth Annual ACM Symposium on the Theory of Computing, pages 135-148, 1974. Google Scholar
  17. Stephen A. Cook and Robert A. Reckhow. The Relative Efficiency of Propositional Proof Systems. Journal of Symbolic Logic, 44:36-50, 1979. Google Scholar
  18. Martin Dowd. Propositional Representation of Arithmetic Proofs. In Proceedings of the 10th ACM Symposium on Theory of Computing (STOC), pages 246-252, 1978. URL: https://doi.org/10.1145/800133.804354.
  19. Erich Grädel. Capturing Complexity Classes by Fragments of Second Order Logic. Theoretical Computer Science, 101:35-57, 1992. Google Scholar
  20. Dmitry Itsykson, Alexander Knop, Andrei E. 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, March 8-11, 2017, Hannover, Germany, pages 43:1-43:14, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.43.
  21. Emil Jeřábek. Dual Weak Pigeonhole Principle, Boolean Complexity, and Derandomization. Annals of Pure and Applied Logic, 124:1-37, 2004. URL: https://doi.org/10.1016/j.apal.2003.12.003.
  22. Jan Johannsen. Satisfiability Problem Complete for Deterministic Logarithmic Space. In Proc. 21st Symp. on Theoretical Aspects of Computer Science (STACS), Lecture Notes in Computer Science 2996, pages 317-325. Springer, 2004. Google Scholar
  23. Stasys Jukna, Alexander A. Razborov, Petr Savický, and Ingo Wegener. On P versus NP ∩ co-NP for Decision Trees and Read-Once Branching Programs. Computational Complexity, 8(4):357-370, 1999. URL: https://doi.org/10.1007/s000370050005.
  24. Alexander Knop. IPS-like proof systems based on binary decision diagrams. Typeset manuscript, June 2017. Google Scholar
  25. Jan Krajíček. Bounded Arithmetic, Propositional Calculus and Complexity Theory. Cambridge University Press, Heidelberg, 1995. Google Scholar
  26. Jan Krajíček. Proof Complexity. Cambridge University Press, 2019. Google Scholar
  27. Jan Krajíček and Pavel Pudlák. Quantified Propositional Calculi and Fragments of Bounded Arithmetic. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 36:29-46, 1990. Google Scholar
  28. Jan Krajíček and Gaisi Takeuti. On Induction-Free Provability. Annals of Mathematics and Artificial Intelligence, pages 107-126, 1992. Google Scholar
  29. Richard E. Ladner. The Circuit Value Problem is Log Space Complete for P. SIGACT News, 7:18-20, 1975. Google Scholar
  30. Jeff B. Paris and Alex J. Wilkie. Counting Problems in Bounded Arithmetic. In Methods in Mathematical Logic, Lecture Notes in Mathematics #1130, pages 317-340. Springer-Verlag, 1985. Google Scholar
  31. Steven Perron. A Propositional Proof System for Log Space. In Proc. 14th Annual Conf. Computer Science Logic (CSL), Springer Verlag Lecture Notes in Computer Science 3634, pages 509-524, 2005. Google Scholar
  32. Steven Perron. Power of Non-Uniformity in Proof Complexity. PhD thesis, Department of Computer Science, University of Toronto, 2009. Google Scholar
  33. G. S. Tsejtin. On the Complexity of Derivation in Propositional Logic. Studies in Constructive Mathematics and Mathematical Logic, 2:115-125, 1968. Google Scholar
  34. Ingo Wegener. Branching Programs and Binary Decision Diagrams. SIAM, 2000. URL: http://ls2-www.cs.uni-dortmund.de/monographs/bdd/.
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