使用最大图割预测BDD操作的内存需求 (扩展论文)
摘要：Adiar利用外部存储器操作二进制决策图（BDD）。这使得处理大型BDD成为可能，但在处理中等大小的BDD时，性能会受到影响。这主要是因为初始化昂贵的外部存储器数据结构，即使它们的内容可以完全适应内部存储器。 这些辅助数据结构的内容始终对应于输入或输出BDD中的一个图形切割。具体而言，这些切割与BDD的层级相对应。我们形式化了这些切割的形状，并为每个BDD操作证明了其最大大小的合理上限。 我们在Adiar中实现了这些上限。通过这些上限，可以预测是否可以使用更快的内部存储器变体的辅助数据结构。在实践中，这提高了Adiar的运行时间。对于中等大小的BDD，计算时间平均减少了86.1\%（中位数为89.7\%）。在某些情况下，差异甚至达到99.9\%。在检查EPFL基准套件中的硬件电路等价性时，某个实例的时间缩短了52小时。
作者：Steffan Christ S{o}lvsten, Jaco van de Pol
论文ID：2307.04488
分类：Data Structures and Algorithms
分类简称：cs.DS
提交时间：2023-07-11