27 May
2021
27 May
'21
10:40 a.m.
Michaël Cadilhac <michael(a)cadilhac.name> writes:
On Wed, May 26, 2021 at 2:52 PM Alexandre Duret-Lutz
<adl(a)lrde.epita.fr> wrote:
One place where Spot spends a lot of time is the conversion of a BDD
into an irredundant sum-of-products. (The implementation is in the
spot::minato_isop class.) This is reportedly a lot faster with ZDDs.
https://doi.org/10.2200/S00612ED1V01Y201411DCS045
Michaël Cadilhac <michael(a)cadilhac.name> writes:
That's super instructive, thanks! I'm not familiar with ZDDs, I'll
have a look into that too. I guess my question is: If you had to go from
scratch today, which BDD
library would you use?
I'd consider either CUDD or Sylvan. CUDD seems to have been unmaintained for quite some
time now,
It still has been maintained for more time than BuDDy, and has been used
in more heavy-duty applications as far as I can tell. TBH the reason I
started with BuDDy initially is just that BDD were new to me and that
BuDDy's C++ interface was a lot simpler (in part because the use of
globals makes it possible to overload C++ operators).
and having parallelism nearly for free with Sylvan is
appealing. As
far as I can (quickly) see, Sylvan is also global-variable-heavy—I
can't really understand how that's still a thing in this day and age…!
I could try to supervise a savvy undergrad or an early grad student on
moving Spot to CUDD or Sylvan; I'll let you know if I find a student.
That's not an easy task: it requires good understanding of the various
ways BDDs are used in Spot, and because they are used everywhere, it's
hard to do the conversion incrementally. If I were to do it, my first
step would be to create a simple "BDD manager class" that initially
dispatches all methods to BuDDy, and just update all the code to use
that class, with the plan to change the BDD manager to use another
backend eventually.