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小时。