Since I started using BDDs in automata, I have faced the following computational problem a few times.  If you have any insight on how to solve it more efficiently, I'd be very interested.  In particular, is there a spot in spot where this is implemented?  Let me spell the problem out in general terms, then tie it to BDDs.

- A collection C of sets over a finite universe U is *unambiguous* if all sets in C are pairwise disjoint.  In other words, C is a partition of the union of its sets.

- A collection C' refines a collection C if each set in C can be obtained as the union of sets in C'.

Given a collection C, compute a (minimal) unambiguous refinement of C.

[[For complexity purposes, the computational task can also be written as:

Given C and k, does there exist an unambiguous refinement of C of size < k?

This is certainly NP-complete ([SP7] in Garey and Johnson is that problem without "unambiguous").]]

Building an unambiguous refinement of BDDs seems an essential step in determinization: If I have a state with two outgoing transitions labeled with BDDs {F, G} such that F&G is not False, then this state is nondeterministic.  To determinize it, we will have to consider the transition labels {F&G, F&!G, !F&G}.  Note that this set refines {F, G}, since F = (F&G)|(F&!G) and similarly for G.

What is known about that problem?  Is there a good heuristic for it that would give an unambiguous refinement not far from the optimal?

I implemented it in a few different ways and would be interested in alternative implementations.  Two options I have are:

1. C' = {U}  (recall that U is our universe, with BDDs this would be True)

2. for each S in C:

3.   for each S' in C':

4.     if (S cap S' is not empty)

5.        Remove S' from C'

6.        Add (S cap S') and (S^c cap S') to C' (^c denotes complement).

  I encode C' as a BDD itself, introducing lots of fresh variables; namely, if C' = {F, G} for two BDDs F and G, I introduce two fresh variables X_F and X_G, and encode C' as (F & X_F) | (G & X_G).  This allows lines 3 and 4 to become:

3. Compute C' & S and project it on the X_? variables.

4. Iterate through each of the variables that appear: if X_S' appears, this means that S cap S' is nonempty.

Thanks for reading!

Cheers,

Michaël