Satisfiability for various branching programs 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.
For Q2:

For Ordered BDDs (OBDD) both satisfiability and counting solutions is polynomial in the size of the OBDD.

For indexed BDD, IBDD p. 16 satisfiability is NP-complete and the equivalence test is coNP-complete even if there are only two layers. 

In general if a variable is read more than one time it is NP-complete if I remember correctly.