A first improvement over the approach of SMV is to use a stack instead of a list to save this references. As an ultimate goal we want to implement non recursive versions of the BDD algorithms. Then the references are accessible on the explicitly modeled call stack and do not have to be saved.
We suggest to investigate how direct hashing works with per level unique tables. It should have a much better memory behaviour than the current scheme.
Also it is possible to leave deleted nodes in the hash table. This would reduce the number of times the whole hash table has to be copied or avoid doubling the unique table during garbage collection at all.
Armin Biere
Mon Apr 20 16:48:53 EDT 1998