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. In a preliminary version of this paper, we provide a satisfiability algorithm for syntactic read- k -times branching programs with n variables and m edges that runs in time O (poly(n, m^k^2)· 2^(1-4^-k-1)n ) . In this paper, we improve the bounds for k = 2. More precisely, we show that the satisfiability of syntactic read-twice branching programs can be solved in time O (poly(n, m)· 2^5n/6 ) . Our algorithm is based on the decomposition technique shown by Borodin, Razborov and Smolensky [Computational Complexity, 1993].