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
Dear Spot devs,
I want to measure how much time it takes Spot to decide whether the
language of the automaton A is contained in that of B.
I've been using the following command
```
autfilt '--stats=%r, %R' A.hoa --included-in=B.hoa
```
I think I am not interpreting the results correctly because `--stats`
reports very small numbers
while adding `time` in front of the command reports much much larger
numbers (several orders of magnitude larger).
What's the right way to measure the time it takes Spot to decide the
inclusion?
Thank you.
Pierre.
