We follow up on the idea of Lars Arge to rephrase the Reduce and Apply procedures of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to simplify and improve the performance of his proposed algorithms. Furthermore, we extend the technique to other common BDD operations, many of which are not derivable using Apply operations alone, and we provide asymptotic improvements for the procedures that can be derived using Apply. These algorithms are implemented in a new BDD package, named Adiar. We see very promising results when comparing the performance of Adiar with conventional BDD package that use recursive depth-first algorithms. For instances larger than 9.5 GiB, our algorithms, in parts using the disk, are 1.47 to 3.69 times slower compared to CUDD and Sylvan, exclusively using main memory. Yet, our proposed techniques are able to obtain this performance at a fraction of the main memory needed by conventional BDD packages to function. Furthermore, with Adiar we are able to manipulate BDDs that outgrow main memory and so surpass the limits of other BDD packages.
翻译:我们跟进了Lars Arge的想法,将二进制决定图(BDDs)的减少和应用程序改写为迭代 I/O-效率算法。我们找出了简化和改进他拟议算法绩效的多种途径。此外,我们将这一技术推广到其他通用的BDD操作,其中许多无法单靠应用操作推断出来,我们为使用应用生成的程序提供了无症状的改进。这些算法是在名为Adiar的新的BDD软件包中实施的。在将Adiar的性能与使用循环深度第一算法的常规BDD软件包进行比较时,我们看到非常有希望的结果。对于超过9.5 GB的功能,我们使用磁盘的部件的算法比CUDDD和Sylvan慢1.47至3.69倍,仅使用主内存。然而,我们提出的技术能够在常规的BDDD软件包所需的主要内存的一小部分内存中取得这种性能。此外,与Adiar相比,我们能够对超出其他BDDDs主内存限度。