[Not-really-Spot] BDD libraries
Hi there ADL & all, Apologies for the not-really-spot question, but the expertise on this list is quite unique! I'm about to embark on a new project that relies on BDD. My only experience with BDD libraries was through using Spot, so I'm familiar with BuDDy, but that's it. Starting something fresh, I'm pondering what's the best C++ BDD library available nowadays. I axed through BuDDy and refactored it so that it's template-only and encapsulated the global variables in a class (hoping for some performance boost from inlining). While I'm fairly happy with the result, I now realize that there's been some progress in the BDD landscape since 1997—crazy! This paper: https://www.tvandijk.nl/pdf/2015setta.pdf by the author of Sylvan seems to indicate that Sylvan offers good performances on a single core, and great perf on multicore. It also comes with a nice C++ interface. I guess my question is: If you had to go from scratch today, which BDD library would you use? Cheers, M.
Michaël Cadilhac <michael@cadilhac.name> writes:
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. Having transitions labeled by BDDs from BuDDy is currently what prevents Spot from supporting multithreaded algorithms easily. Having the global in a class, like CUDD or what you did, would at least allow to run independent BDD computations in parallel. Also there are some algorithms in Spot that would benefit from using ZDDs instead of BDDs. Getting rid of BuDDy has been a wish for a very long time, but it's just so pervasive in Spot that it would take a lot work. Also note that the version of BuDDy distributed with Spot has also diverged a lot from the "upstream" BuDDy. I reduced the memory footprint of the BDD nodes to improve caching, derecursived several algorithms to reduce stack overflows, and introduced a few algorithms needed by Spot (e.g. the development version of Spot now has a way to iterate over all minterms of a BDD that is much faster than what we used to do before). These small improvements are easier to do than getting rid of BuDDy :-( Best,
On Wed, May 26, 2021 at 2:52 PM Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
Michaël Cadilhac <michael@cadilhac.name> writes:
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.
That's super instructive, thanks! I'm not familiar with ZDDs, I'll have a look into that too. CUDD seems to have been unmaintained for quite some time now, 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. Cheers, M.
Michaël Cadilhac <michael@cadilhac.name> writes:
On Wed, May 26, 2021 at 2:52 PM Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
Michaël Cadilhac <michael@cadilhac.name> writes:
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.
That's super instructive, thanks! I'm not familiar with ZDDs, I'll have a look into that too.
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
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.
participants (2)
-
Alexandre Duret-Lutz -
Michaël Cadilhac