eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-12-07
58:1
58:10
10.4230/LIPIcs.ISAAC.2017.58
article
Satisfiability Algorithm for Syntactic Read-$k$-times Branching Programs
Nagao, Atsuki
Seto, Kazuhisa
Teruyama, Junichi
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].
https://drops.dagstuhl.de/storage/00lipics/lipics-vol092-isaac2017/LIPIcs.ISAAC.2017.58/LIPIcs.ISAAC.2017.58.pdf
branching program
read-k-times
satisfiability
moderately exponential time
polynomial space