The BDD package Adiar manipulates Binary Decision Diagrams (BDDs) in external memory. This enables handling big BDDs, but the performance suffers when dealing with moderate-sized BDDs. This is mostly due to initializing expensive external memory data structures, even if their contents can fit entirely inside internal memory. The contents of these auxiliary data structures always correspond to a graph cut in an input or output BDD. Specifically, these cuts respect the levels of the BDD. We formalise the shape of these cuts and prove sound upper bounds on their maximum size for each BDD operation. We have implemented these upper bounds within Adiar. With these bounds, it can predict whether a faster internal memory variant of the auxiliary data structures can be used. In practice, this improves Adiar's running time across the board. Specifically for the moderate-sized BDDs, this results in an average reduction of the computation time by 86.1% (median of 89.7%). In some cases, the difference is even 99.9\%. When checking equivalence of hardware circuits from the EPFL Benchmark Suite, for one of the instances the time was decreased by 52 hours.

翻译：BDD软件包Adiar在外存中操作二叉决策图（BDD）。这使得处理大规模BDD成为可能，但处理中等规模BDD时性能会下降。这主要是因为初始化昂贵的外存数据结构所致——即便其内容完全可容纳于内存中。这些辅助数据结构的内容始终对应输入或输出BDD中的图割。具体而言，这些割遵循BDD的层级结构。我们形式化定义了这些割的形状，并为每个BDD操作证明了其最大规模的可靠上界。我们在Adiar中实现了这些上界。凭借这些边界，Adiar可预判是否能够使用更快速的内存型辅助数据结构。实际应用中，该优化全面提升了Adiar的运行时间。对于中等规模BDD，平均计算时间减少86.1%（中位数89.7%），某些情况下甚至达到99.9%。在EPFL基准测试套件的硬件电路等价性检验中，某个实例的计算时间缩短了52小时。