Counting words that satisfy SAT-like constraints with BDDs

Question

I have the following #P-complete problem:

Given an alphabet $\Sigma$ and a matrix $M$ where each entry can be a symbol from $\Sigma$ or the wildcard symbol $*$, find the number of strings $s$ with the property that there exists $i$ such that for all $j$, $M_{i,j} \neq *$ implies $s_j = M_{i,j}$.

Example: If $\Sigma = \{a,b,c\}$ and $M$ = $$\left(\begin{matrix} a&*&b \\ *&c&* \end{matrix} \right)$$ then there are three satisfying strings: $aab,abb,acb$.

I was told this can be solved using BDDs, somehow, such that a lot of caching is possible. How does that work? Also, what are other algorithms for this?

Proof of #P-completeness: We reduce from #UNSAT, the problem of counting the number of unsatisfying assignments for a boolean formula. Given a formula $\varphi$ with $n$ variables and $m$ clauses, make an $m$ by $n$ matrix $M$ over the alphabet $\Sigma = \{0,1\}$ such that $$M_{i,j} = \begin{cases} 1\text{ if the $j^{th}$ literal is unnegated in the $i^{th}$ clause,} \\ 0\text{ if the $j^{th}$ literal is negated in the $i^{th}$ clause,} \\ *\text{ otherwise.} \end{cases} $$ Then the number of strings with the above property equals the number of unsatisfying assignments for $\varphi$.

Answer 1

Yes, you can use a BDD to solve this, but BDD's aren't magic: they don't magically allow you to solve a #P-complete problem efficiently. You can use BDD's to solve this, but the resulting solution might be highly inefficient.

How do you use BDD's to solve this? Broadly, you build a BDD that represents all strings that satisfy the property, and then you count how many strings are accepted by this BDD.

To learn how to build a BDD that accepts all strings that satisfy the property, I suggest that you study basic material on BDDs. The key property that's relevant here is that given BDDs for the sets $S,S'$, it is easy to construct a BDD for the set $S \cup S'$. So, you build a BDD for the set of strings that are accepted by each row of the matrix, and then you take their union to get a BDD for the union. Beware that the resulting BDD could have exponential size.

Once you have a BDD, it's easy to count the number of strings accepted by a BDD. It's an especially simple application of dynamic programming: for each node $n$ in the BDD, you count the number of paths from $n$ to some leaf. These numbers can be filled in by visiting the nodes in bottom-up order, and using dynamic programming.

There's nothing fancy here. Once you are familiar with BDD's, everything here should look bog-standard. So, if this looks mysterious, I recommend you spend some quality time with a textbook that explains how BDD's work.

---

Other algorithms: you could also use any algorithm for #SAT. There are off-the-shelf algorithms and tools for computing #SAT. It's straightforward to translate your problem to an instance of #SAT, and then apply one of those tools. See, e.g., https://cstheory.stackexchange.com/q/1295/5038, Is there a sometimes-efficient algorithm to solve #SAT?, https://cstheory.stackexchange.com/q/18135/5038.