From: Jimmy <u4308348@an...> - 2011-04-27 00:48:09
Hi, I'm a new user of BuDDy, and I've found that with as few as 70 BDD
variables, I'm tending towards using several gigabytes of memory,
millions of nodes (as reported by the GC), and a nontrivial amount of
time to and- together some 25 relatively small (3 or 4 variable nodes
when printed) formulae.
Is this common behaviour? Is there a better way to calculate the
conjunction of a collection of formulae? Could this be somehow due to me
using the OCaml bindings, rather than C/++?
I am implementing my own version of someone else's algorithm as a
prelude to modifying it, and I know that their implementation can handle
the particular instance I am trying within 20 seconds, while my version
is taking several minutes and more memory. However I don't know whether
they use another BDD package which may be better, or whether they use
other tricks and tweaks to improve performance which I'm not aware of.