Document Open Access Logo

Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs

Authors Ludmila Glinskih, Dmitry Itsykson

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.26.pdf
  • Filesize: 464 kB
  • 12 pages

Document Identifiers

Author Details

Ludmila Glinskih
Dmitry Itsykson

Cite AsGet BibTex

Ludmila Glinskih and Dmitry Itsykson. Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 26:1-26:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.MFCS.2017.26

Abstract

We consider satisfiable Tseitin formulas TS_{G,c} based on d-regular expanders G with the absolute value of the second largest eigenvalue less than d/3. We prove that any nondeterministic read-once branching program (1-NBP) representing TS_{G,c} has size 2^{\Omega(n)}, where n is the number of vertices in G. It extends the recent result by Itsykson at el. [STACS 2017] from OBDD to 1-NBP. On the other hand it is easy to see that TS_{G,c} can be represented as a read-2 branching program (2-BP) of size O(n), as the negation of a nondeterministic read-once branching program (1-coNBP) of size O(n) and as a CNF formula of size O(n). Thus TS_{G,c} gives the best possible separations (up to a constant in the exponent) between 1-NBP and 2-BP, 1-NBP and 1-coNBP and between 1-NBP and CNF.
Keywords
  • Tseitin formula
  • read-once branching program
  • expander

Metrics

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

References

  1. Noga Alon and Fan R. K. Chung. Explicit construction of linear sized tolerant networks. Discrete Mathematics, 306(10-11):1068-1071, 2006. URL: http://dx.doi.org/10.1016/j.disc.2006.03.025.
  2. L. Babai, P. Hajnal, E. Szemeredi, and G. Turan. A lower bound for read-once-only branching programs. Journal of Computer and System Sciences, 35:153-162, 1987. Google Scholar
  3. Eli Ben-Sasson. Hard examples for bounded depth Frege. In Proceedings on 34th Annual ACM Symposium on Theory of Computing, May 19-21, 2002, Montréal, Québec, Canada, pages 563-572, 2002. URL: http://dx.doi.org/10.1145/509907.509988.
  4. Allan Borodin, Alexander A. Razborov, and Roman Smolensky. On lower bounds for read-k-times branching programs. Computational Complexity, 3:1-18, 1993. URL: http://dx.doi.org/10.1007/BF01200404.
  5. J Cheeger. A lower bound for the smallest eigenvalue of the laplacian. Problems Anal., page 195, 1970. Google Scholar
  6. Stephen A. Cook, Jeff Edmonds, Venkatesh Medabalimi, and Toniann Pitassi. Lower bounds for nondeterministic semantic read-once branching programs. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, pages 36:1-36:13, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.36.
  7. 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.
  8. D.M. Itsykson and A.A. Kojevnikov. Lower bounds of static Lovasz-Schrijver calculus proofs for Tseitin tautologies. Zapiski Nauchnykh Seminarov POMI, 340:10-32, 2006. Google Scholar
  9. Dmitry Itsykson, Alexander Knop, Andrei 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: http://dx.doi.org/10.4230/LIPIcs.STACS.2017.43.
  10. Stasys Jukna. A note on read-k times branching programs. ITA, 29(1):75-83, 1995. Google Scholar
  11. Stasys Jukna. A nondeterministic space-time tradeoff for linear codes. Inf. Process. Lett., 109(5):286-289, 2009. URL: http://dx.doi.org/10.1016/j.ipl.2008.11.001.
  12. László Lovász, Moni Naor, Ilan Newman, and Avi Wigderson. Search Problems in the Decision Tree Model. SIAM J. Discrete Math., 8(1):119-132, 1995. URL: http://dx.doi.org/10.1137/S0895480192233867.
  13. A Lubotzky, R Phillips, and P Sarnak. Ramanujan graphs. Combinatorica, 8(3):261-277, 1988. Google Scholar
  14. EA Okolnishnikova. On lower bounds for branching programs. Siberian Advances in Mathematics, 3(1):152-166, 1993. Google Scholar
  15. Toniann Pitassi, Benjamin Rossman, Rocco A. Servedio, and Li-Yang Tan. Poly-logarithmic Frege depth lower bounds via an expander switching lemma. In Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, Cambridge, MA, USA, June 18-21, 2016, pages 644-657, 2016. URL: http://dx.doi.org/10.1145/2897518.2897637.
  16. Jayram S. Thathachar. On separating the read-k-times branching program hierarchy. In Proceedings of the Thirtieth Annual ACM Symposium on the Theory of Computing, Dallas, Texas, USA, May 23-26, 1998, pages 653-662, 1998. URL: http://dx.doi.org/10.1145/276698.276881.
  17. A. Urquhart. Hard examples for resolution. JACM, 34(1):209-219, 1987. Google Scholar
  18. Ingo Wegener. Branching Programs and Binary Decision Diagrams. SIAM, 2000. Google Scholar
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