<p>For Q2:</p>

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

<p>For indexed BDD, <a href="http://web.cecs.pdx.edu/~mperkows/PerkowskiGoogle/drechselr-10030112.pdf" rel="nofollow">IBDD p. 16</a> satisfiability is NP-complete and the equivalence test is coNP-complete even if there are only two layers. </p>

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

CC BY-SA 3.0
2014-06-20T14:37:50.503Z
2014-06-20T14:49:12.120Z
2014-06-20T14:49:12.120Z
joro
<p>Clearly, SAT for CNF, formula, or many classes of boolean circuits have strong significance on the entire theory community.</p>
<p>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 <span class="math-container">$S(n)$</span> are simulated by  branching program of size <span class="math-container">$2^{S(n)}$</span>.</p>
<p>My question is about  classification of hardness of <span class="math-container">$satisfiability$</span> problem for <span class="math-container">$branching$</span> <span class="math-container">$programs$</span>.</p>
<p>More concretely,</p>
<blockquote>
<p>Q1. SAT for branching programs corresponding natural complexity classes like <span class="math-container">$L/poly$</span>, <span class="math-container">$NL/poly$</span>, or <span class="math-container">$\oplus L/poly$</span> can be computed polynomial time ?</p>
<p>Q2. Is there some <span class="math-container">$threshold$</span> <span class="math-container">$condition$</span> for BP-SAT problem ? For example, I hope some results as follows: for some two classes of branching programs <span class="math-container">$\mathcal{C},\mathcal{D}$</span>, one of two is polytime computable and the other one is NP hard.</p>
</blockquote>

CC BY-SA 3.0
2014-06-21T02:14:14.637Z
Satisfiability for branching programs in many cases reduces to graph connectivity. e.g. directed connectivity is complete for NL.
Thomas Steinke
<sat><boolean-functions><space-bounded><space-complexity>
Satisfiability for various branching programs
Shen
# Satisfiability for various branching programs

(Asked by: username_0 on 2014-06-20)

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.

**Tags:** sat, boolean-functions, space-bounded, space-complexity

> **Comments:**
> **username_1**: Satisfiability for branching programs in many cases reduces to graph connectivity. e.g. directed connectivity is complete for NL.  

---

## 1 answers

### Answer by username_2 on 2014-06-20. Score: 4 | Accepted answer

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](http://web.cecs.pdx.edu/~mperkows/PerkowskiGoogle/drechselr-10030112.pdf) 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.


---

