# Counting words that satisfy SAT-like constraints with BDDs

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$.

• I'm sorry, but I don't know what "some $i$ and all $j$ means". Does that mean $\exists i \forall j$? $\forall j \exists i$? The two are not equivalent. I suggest you edit the question to state the property more precisely. – D.W. Dec 21 '15 at 1:34
• @D.W. The former. In other words, the string only has to satisfy one row of the matrix; each row can be thought of as a "clause" and the matrix as a DNF-type formula. That's why it's #P-complete: counting models to DNF formulae is #P-complete, and if you limit the alphabet to {0,1}, then the matrix is exactly like DNF. – Elliot Gorokhovsky Dec 21 '15 at 2:00

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.

• What kinds of sub-trees can you cache? I'm interested in a particular case, I'll edit my question. – Elliot Gorokhovsky Dec 21 '15 at 4:37
• @RenéG, if you want to know how to count how many strings are accepted by a BDD, I recommend you spend some time reading about BDD's (e.g., from a textbook), then if you still can't see how to do it, ask a new question... and show what approaches you've considered. – D.W. Dec 21 '15 at 9:38