Document Open Access Logo

Branching Programs with Bounded Repetitions and Flow Formulas

Authors Anastasia Sofronova, Dmitry Sokolov

PDF
Thumbnail PDF

File

LIPIcs.CCC.2021.17.pdf
  • Filesize: 0.87 MB
  • 25 pages

Document Identifiers

Author Details

Anastasia Sofronova
  • St. Petersburg Department of Steklov Mathematical Institute of, Russian Academy of Sciences, Russia
Dmitry Sokolov
  • St. Petersburg Department of Steklov Mathematical Institute of, Russian Academy of Sciences, Russia
  • St. Petersburg State University, Russia

Funding

  • Sofronova, Anastasia: The research presented in Sections 3 and 4 is supported by Russian Science Foundation (project 18-71-10042).

Acknowledgements

The authors would like to thank Dmitry Itsykson, Artur Riazanov for fruitful discussions and comments, Edward Hirsch for comments on the draft, Alexander Knop for a statement of the problem. The authors would also like to thank anonymous reviewers for their valuable comments.

Cite As Get BibTex

Anastasia Sofronova and Dmitry Sokolov. Branching Programs with Bounded Repetitions and Flow Formulas. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 17:1-17:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CCC.2021.17

Abstract

Restricted branching programs capture various complexity measures like space in Turing machines or length of proofs in proof systems. In this paper, we focus on the application in the proof complexity that was discovered by Lovasz et al. [László Lovász et al., 1995] who showed the equivalence between regular Resolution and read-once branching programs for "unsatisfied clause search problem" (Search_φ). This connection is widely used, in particular, in the recent breakthrough result about the Clique problem in regular Resolution by Atserias et al. [Albert Atserias et al., 2018].
We study the branching programs with bounded repetitions, so-called (1,+k)-BPs (Sieling [Detlef Sieling, 1996]) in application to the Search_φ problem. On the one hand, it is a natural generalization of read-once branching programs. On the other hand, this model gives a powerful proof system that can efficiently certify the unsatisfiability of a wide class of formulas that is hard for Resolution (Knop [Alexander Knop, 2017]).
We deal with Search_φ that is "relatively easy" compared to all known hard examples for the (1,+k)-BPs. We introduce the first technique for proving exponential lower bounds for the (1,+k)-BPs on Search_φ. To do it we combine a well-known technique for proving lower bounds on the size of branching programs [Detlef Sieling, 1996; Detlef Sieling and Ingo Wegener, 1994; Stasys Jukna and Alexander A. Razborov, 1998] with the modification of the "closure" technique [Michael Alekhnovich et al., 2004; Michael Alekhnovich and Alexander A. Razborov, 2003]. In contrast with most Resolution lower bounds, our technique uses not only "local" properties of the formula, but also a "global" structure. Our hard examples are based on the Flow formulas introduced in [Michael Alekhnovich and Alexander A. Razborov, 2003].

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • branching programs
  • bounded repetitions
  • lower bounds

Metrics

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

Related Versions

References

  1. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Pseudorandom generators in propositional proof complexity. SIAM J. Comput., 34(1):67-88, 2004. URL: https://doi.org/10.1137/S0097539701389944.
  2. Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart. An exponential separation between regular and general resolution. Theory Comput., 3(1):81-102, 2007. URL: https://doi.org/10.4086/toc.2007.v003a005.
  3. Michael Alekhnovich and Alexander A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. Proceedings of the Steklov Institute of Mathematics, 242:18-35, 2003. Available at http://people.cs.uchicago.edu/~razborov/files/misha.pdf. Preliminary version in FOCS '01.
  4. Noga Alon and Fan R. K. Chung. Explicit construction of linear sized tolerant networks. Discret. Math., 72(1-3):15-19, 1988. URL: https://doi.org/10.1016/0012-365X(88)90189-6.
  5. Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Alexander A. Razborov. Clique is hard on average for regular resolution. In Ilias Diakonikolas, David Kempe, and Monika Henzinger, editors, Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los Angeles, CA, USA, June 25-29, 2018, pages 866-877. ACM, 2018. URL: https://doi.org/10.1145/3188745.3188856.
  6. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. URL: https://doi.org/10.1145/375827.375835.
  7. Stephen Cook and Robert Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, March 1979. URL: https://projecteuclid.org:443/euclid.jsl/1183740343.
  8. L. R. Ford and D. R. Fulkerson. Maximal flow through a network. Canadian Journal of Mathematics, 8:399-404, 1956. URL: https://doi.org/10.4153/CJM-1956-045-5.
  9. Konstantinos Georgiou, Avner Magen, and Madhur Tulsiani. Optimal sherali-adams gaps from pairwise independence. In Irit Dinur, Klaus Jansen, Joseph Naor, and José Rolim, editors, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques, pages 125-139, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  10. Stasys Jukna. Expanders and time-restricted branching programs. Theor. Comput. Sci., 409(3):471-476, 2008. URL: https://doi.org/10.1016/j.tcs.2008.09.012.
  11. Stasys Jukna. Boolean Function Complexity - Advances and Frontiers, volume 27 of Algorithms and combinatorics. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-24508-4.
  12. Stasys Jukna and Alexander A. Razborov. Neither reading few bits twice nor reading illegally helps much. Discret. Appl. Math., 85(3):223-238, 1998. URL: https://doi.org/10.1016/S0166-218X(98)00042-0.
  13. Alexander Knop. IPS-like Proof Systems Based on Binary Decision Diagrams. Electron. Colloquium Comput. Complex., 24:179, 2017. URL: https://eccc.weizmann.ac.il/report/2017/179.
  14. László Lovász, Moni Naor, Ilan Newman, and Avi Wigderson. Search problems in the decision tree model. SIAM J. Discret. Math., 8(1):119-132, 1995. URL: https://doi.org/10.1137/S0895480192233867.
  15. William Masek. A fast algorithm for the string editing problem and decision graph complexity. Master Thesis, Massachusetts Institute of Technology, 1976. Google Scholar
  16. E. I. Nechiporuk. On a boolean function. Dokl. Akad. Nauk SSSR, 169:765-766, 1966. Google Scholar
  17. Toniann Pitassi and Ran Raz. Regular resolution lower bounds for the weak pigeonhole principle. Comb., 24(3):503-524, 2004. URL: https://doi.org/10.1007/s00493-004-0030-y.
  18. Ran Raz. Resolution lower bounds for the weak pigeonhole principle. J. ACM, 51(2):115-138, 2004. URL: https://doi.org/10.1145/972639.972640.
  19. Petr Savický. A probabilistic nonequivalence test for syntactic (1,+k)-branching programs. Electron. Colloquium Comput. Complex., 5(51), 1998. URL: http://eccc.hpi-web.de/eccc-reports/1998/TR98-051/index.html.
  20. Petr Savický and Stanislav Žák. A lower bound on branching programs reading some bits twice. Theor. Comput. Sci., 172(1-2):293-301, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00183-1.
  21. Detlef Sieling. New lower bounds and hierarchy results for restricted branching programs. J. Comput. Syst. Sci., 53(1):79-87, 1996. URL: https://doi.org/10.1006/jcss.1996.0050.
  22. Detlef Sieling and Ingo Wegener. New lower bounds and hierarchy results for restricted branching programs. In Ernst W. Mayr, Gunther Schmidt, and Gottfried Tinhofer, editors, Graph-Theoretic Concepts in Computer Science, 20th International Workshop, WG '94, Herrsching, Germany, June 16-18, 1994, Proceedings, volume 903 of Lecture Notes in Computer Science, pages 359-370. Springer, 1994. URL: https://doi.org/10.1007/3-540-59071-4_61.
  23. Dmitry Sokolov. (semi)algebraic proofs over ±1 variables. In Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy, editors, Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, pages 78-90. ACM, 2020. URL: https://doi.org/10.1145/3357713.3384288.
  24. Ingo Wegener. On the complexity of branching programs and decision trees for clique functions. J. ACM, 35(2):461-471, 1988. URL: https://doi.org/10.1145/42282.46161.
  25. Ingo Wegener. Branching Programs and Binary Decision Diagrams. SIAM, 2000. URL: http://ls2-www.cs.uni-dortmund.de/monographs/bdd/.
  26. Stanislav Žák. An exponential lower bound for real-time branching programs. Information and Control, 71(1):87-94, 1986. URL: https://doi.org/10.1016/S0019-9958(86)80018-3.
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