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