25 May
2021
25 May
'21
8:08 p.m.
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.
26 May
26 May
9:52 p.m.
Michaël Cadilhac <michael(a)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,
10:19 p.m.
On Wed, May 26, 2021 at 2:52 PM Alexandre Duret-Lutz <adl(a)lrde.epita.fr> wrote:
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.
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.
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.
27 May
27 May
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.
1350
days inactive
1352
days old
3 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Michaël Cadilhac