Document Open Access Logo

Satisfiability Algorithm for Syntactic Read-$k$-times Branching Programs

Authors Atsuki Nagao, Kazuhisa Seto, Junichi Teruyama

PDF
Thumbnail PDF

File

LIPIcs.ISAAC.2017.58.pdf
  • Filesize: 467 kB
  • 10 pages

Document Identifiers

Author Details

Atsuki Nagao
Kazuhisa Seto
Junichi Teruyama

Cite AsGet BibTex

Atsuki Nagao, Kazuhisa Seto, and Junichi Teruyama. Satisfiability Algorithm for Syntactic Read-$k$-times Branching Programs. In 28th International Symposium on Algorithms and Computation (ISAAC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 92, pp. 58:1-58:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ISAAC.2017.58

Abstract

The satisfiability of a given branching program is to determine whether there exists a consistent path from the root to 1-sink. In a syntactic read-k-times branching program, each variable appears at most k times in any path from the root to a sink. We provide a satisfiability algorithm for syntactic read-k-times branching programs with n variables and m edges that runs in time O\left(\poly(n, m^{k^2})\cdot 2^{(1-\mu(k))n}\right), where \mu(k) = \frac{1}{4^{k+1}}. Our algorithm is based on the decomposition technique shown by Borodin, Razborov and Smolensky [Computational Complexity, 1993].
Keywords
  • branching program
  • read-k-times
  • satisfiability
  • moderately exponential time
  • polynomial space

Metrics

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

References

  1. Amir Abboud, Thomas Dueholm Hansen, Virginia Vassilevska Williams, and Ryan Williams. Simulating branching programs with edit distance and friends: or: a polylog shaved is a lower bound made. In Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC, pages 375-388, 2016. Google Scholar
  2. Vikraman Arvind and Rainer Schuler. The quantum query complexity of 0-1 knapsack and associated claw problems. In Proceedings of the 14th International Symposium on Algorithms and Computation (ISAAC), pages 168-177, 2003. Google Scholar
  3. David A. Mix Barrington. Bounded-width polynomial-size branching programs recognize exactly those languages in nc¹. J. Comput. Syst. Sci., 38(1):150-164, 1989. Google Scholar
  4. Paul Beame, Russell Impagliazzo, and Srikanth Srinivasan. Approximating AC⁰ by small height decision trees and a deterministic algorithm for #AC⁰ SAT. In Proceedings of the 27th Conference on Computational Complexity (CCC), pages 117-125, 2012. Google Scholar
  5. Paul Beame, T. S. Jayram, and Michael E. Saks. Time-space tradeoffs for branching programs. J. Comput. Syst. Sci., 63(4):542-572, 2001. Google Scholar
  6. Beate Bollig, Martin Sauerhoff, Detlef Sieling, and Ingo Wegener. Hierarchy theorems for kobdds and kibdds. Theoretical Computer Science, 205(1-2):45-60, 1998. Google Scholar
  7. Allan Borodin, Alexander A. Razborov, and Roman Smolensky. On lower bounds for read-k-times branching programs. Computational Complexity, 3:1-18, 1993. Google Scholar
  8. Chris Calabro, Russell Impagliazzo, and Ramamohan Paturi. A duality between clause width and clause density for SAT. In Proceedings of the 21st Annual IEEE Conference on Computational Complexity (CCC), pages 252-260, 2006. Google Scholar
  9. Chris Calabro, Russell Impagliazzo, and Ramamohan Paturi. The complexity of satisfiability of small depth circuits. In Revised Selected Papers from the 4th International Workshop on Parameterized and Exact Computation, volume 5917 of LNCS, pages 75-85, 2009. Google Scholar
  10. Ruiwen Chen, Valentine Kabanets, Antonina Kolokolova, Ronen Shaltiel, and David Zuckerman. Mining circuit lower bound proofs for meta-algorithms. In Proceedings of the 21st Annual IEEE Conference on Computational Complexity (CCC), pages 262-273, 2014. Google Scholar
  11. Ruiwen Chen, Valentine Kabanets, and Nitin Saurabh. An improved deterministic #SAT algorithm for small De Morgan formulas. In Proceedings of the 39th International Symposium on Mathematical Foundations of Computer Science (MFCS), Part II, pages 165-176, 2014. Google Scholar
  12. Evgeny Dantsin, Edward A. Hirsch, and Alexander Wolpert. Algorithms for SAT based on search in Hamming balls. In Proceedings of the 21st Annual Symposium on Theoretical Aspects of Computer Science (STACS), pages 141-151, 2004. Google Scholar
  13. Evgeny Dantsin, Edward A. Hirsch, and Alexander Wolpert. Clause shortening combined with pruning yields a new upper bound for deterministic SAT algorithms. In Proceedings of the 6th International Conference on Algorithms and Complexity (CIAC), pages 60-68, 2006. Google Scholar
  14. Edward A. Hirsch. Exact algorithms for general CNF SAT. In Encyclopedia of Algorithms. 2008. Google Scholar
  15. Russell Impagliazzo, William Matthews, and Ramamohan Paturi. A satisfiability algorithm for AC⁰. In Proceedings of the 23rd Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 961-972, 2012. Google Scholar
  16. Russell Impagliazzo, Ramamohan Paturi, and Stefan Schneider. A satisfiability algorithm for sparse depth two threshold circuits. In Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pages 479-488, 2013. Google Scholar
  17. Stasys Jukna. A note on read-k times branching programs. ITA, 29(1):75-83, 1995. Google Scholar
  18. Atsuki Nagao, Kazuhisa Seto, and Junichi Teruyama. A moderately exponential time algorithm for k-IBDD satisfiability. In Proceedings of Algorithms and Data Structures - 14th International Symposium (WADS), pages 554-565, 2015. Google Scholar
  19. Pavel Pudlák. Satisfiability - algorithms and logic. In Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS), pages 129-141, 1998. Google Scholar
  20. Rahul Santhanam. Fighting perebor: New and improved algorithms for formula and QBF satisfiability. In Proceedings of the 51th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pages 183-192, 2010. Google Scholar
  21. Martin Sauerhoff. Lower bounds for randomized read-k-times branching programs. In Proceedings of the 15th Annual Symposium on Theoretical Aspects of Computer Science (STACS), pages 105-115, 1998. Google Scholar
  22. Rainer Schuler. An algorithm for the satisfiability problem of formulas in conjunctive normal form. Journal of Algorithms, 54(1):40-44, 2005. Google Scholar
  23. Kazuhisa Seto and Suguru Tamaki. A satisfiability algorithm and average-case hardness for formulas over the full binary basis. Computational Complexity, 22(2):245-274, 2013. Google Scholar
  24. Avishay Tal. #SAT algorithms from shrinkage. Electronic Colloquium on Computational Complexity (ECCC), 22(114), 2015. Google Scholar
  25. Jayram S. Thathachar. On separating the read-k-times branching program hierarchy. In Proceedings of the 30th Annual ACM Symposium on the Theory of Computing (STOC), pages 653-662, 1998. Google Scholar
  26. Ryan Williams. Improving exhaustive search implies superpolynomial lower bounds. SIAM J. Comput., 42(3):1218-1244, 2013. Google Scholar
  27. Ryan Williams. Nonuniform ACC circuit lower bounds. Journal of ACM, 61(1):2:1-2:32, 2014. 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