使用最大图割预测BDD操作的内存需求（扩展论文）
Predicting Memory Demands of BDD Operations using Maximum Graph Cuts (Extended Paper)
AI总结：
针对外部内存BDD工具Adiar处理中等规模BDD时性能不佳的问题，研究通过形式化BDD操作对应的图割形态并证明其最大规模上界，实现内存需求预测以选择更优存储结构，大幅提升了运行效率。
摘要：
BDD软件包Adiar在外部存储器中操作二元决策图（Binary Decision Diagrams，BDD）。这一机制能够处理大型BDD，但在处理中等规模BDD时性能会受到影响，主要原因是即便外部存储器数据结构的内容可以完全装入内存，仍需初始化开销高昂的这类结构。\n这些辅助数据结构的内容始终对应输入或输出BDD中的一个图割，具体而言，这些割满足BDD的层级约束。我们形式化了这类割的形态，并证明了每种BDD操作下其最大规模的可靠上界。\n我们已在Adiar中实现了这些上界。借助这些上界，程序可以预测是否能够使用速度更快的内存版辅助数据结构。实际应用中，这全面提升了Adiar的运行速度：针对中等规模BDD，计算时间平均减少86.1%（中位数为89.7%），部分场景下降幅甚至达到99.9%；在对EPFL基准测试套件中的硬件电路进行等价性检查时，其中一个实例的运行时间减少了52小时。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
