[Spot] Unambiguous refinements of collections of BDDs

Michaël Cadilhac michael at cadilhac.name
Fri Jul 16 12:36:45 CEST 2021


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20210716/b15e6533/attachment.htm>


More information about the Spot mailing list