Hi there all,
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.
*Definitions.*
- 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'.
*Problem.*
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").]]
*Motivation.*
In BDDs, my use case is to have C be a collection of BDDs and a BDD
represent the set of its satisfying assignments.
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.
*Question.*
What is known about that problem? Is there a good heuristic for it that
would give an unambiguous refinement not far from the optimal?
*Implementations.*
I implemented it in a few different ways and would be interested in
alternative implementations. Two options I have are:
*- The straightforward way:*
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).
*- A slightly more complex implementation.*
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
