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 5 n / 6 . Our algorithm is based on the decomposition technique shown by Borodin, Razborov and Smolensky [Computational Complexity, 1993]. [ABSTRACT FROM AUTHOR]