Clearly, SAT for CNF, formula, or many classes of boolean circuits have strong significance on the entire theory community.
Branching program, or BDD is one of the most basic and popular computational models for boolean functions. For instance, arbitrary space bounded TM with space $S(n)$ are simulated by branching program of size $2^{S(n)}$.
My question is about classification of hardness of $satisfiability$ problem for $branching$ $programs$.
More concretely,
Q1. SAT for branching programs corresponding natural complexity classes like $L/poly$, $NL/poly$, or $\oplus L/poly$ can be computed polynomial time ?
Q2. Is there some $threshold$ $condition$ for BP-SAT problem ? For example, I hope some results as follows: for some two classes of branching programs $\mathcal{C},\mathcal{D}$, one of two is polytime computable and the other one is NP hard.