Satisfiability Algorithm for Syntactic Read-$k$-times Branching Programs
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].
branching program
read-k-times
satisfiability
moderately exponential time
polynomial space
58:1-58:10
Regular Paper
Atsuki
Nagao
Atsuki Nagao
Kazuhisa
Seto
Kazuhisa Seto
Junichi
Teruyama
Junichi Teruyama
10.4230/LIPIcs.ISAAC.2017.58
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.
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.
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.
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.
Paul Beame, T. S. Jayram, and Michael E. Saks. Time-space tradeoffs for branching programs. J. Comput. Syst. Sci., 63(4):542-572, 2001.
Beate Bollig, Martin Sauerhoff, Detlef Sieling, and Ingo Wegener. Hierarchy theorems for kobdds and kibdds. Theoretical Computer Science, 205(1-2):45-60, 1998.
Allan Borodin, Alexander A. Razborov, and Roman Smolensky. On lower bounds for read-k-times branching programs. Computational Complexity, 3:1-18, 1993.
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.
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.
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.
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.
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.
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.
Edward A. Hirsch. Exact algorithms for general CNF SAT. In Encyclopedia of Algorithms. 2008.
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.
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.
Stasys Jukna. A note on read-k times branching programs. ITA, 29(1):75-83, 1995.
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.
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.
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.
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.
Rainer Schuler. An algorithm for the satisfiability problem of formulas in conjunctive normal form. Journal of Algorithms, 54(1):40-44, 2005.
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.
Avishay Tal. #SAT algorithms from shrinkage. Electronic Colloquium on Computational Complexity (ECCC), 22(114), 2015.
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.
Ryan Williams. Improving exhaustive search implies superpolynomial lower bounds. SIAM J. Comput., 42(3):1218-1244, 2013.
Ryan Williams. Nonuniform ACC circuit lower bounds. Journal of ACM, 61(1):2:1-2:32, 2014.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode