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的运行效率。特别对于中等规模BDD，计算时间平均减少86.1%（中位数89.7%）。在某些案例中差异甚至达到99.9%。在对EPFL基准测试集中的硬件电路进行等价性验证时，其中一个实例的处理时间缩短了52小时。