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.

  • 1
    $\begingroup$ Satisfiability for branching programs in many cases reduces to graph connectivity. e.g. directed connectivity is complete for NL. $\endgroup$
    – Thomas
    Jun 21, 2014 at 2:14

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.