Multi-variable Quantification of BDDs in External Memory using Nested Sweeping

doi:10.1007/978-3-032-15700-3_17

2026-01-01

PRE

Steffan Christ Sølvsten *

Jaco van de Pol

DOI：10.1007/978-3-032-15700-3_17

原文链接

原文求助

摘要

En 中文

对Adiar BDD软件包的先前研究成功地设计了能够处理存储在外部内存中的大型二元决策图(BDDs)的算法。为此，它通过连续扫描BDDs来解决计算。然而，这种方法使其算法未能涵盖多变量量化、关系积和变量重排序的范畴。在本工作中，我们通过引入嵌套扫描框架来解决这一问题。在此框架中，多个并发扫描相互传递信息以计算结果。我们在Adiar中实现了该框架，并利用它创建了一种新的外部内存多变量量化算法。在实践中，这使Adiar的运行时间缩短了1.7倍。反过来，这项工作将Adiar的先前研究成果扩展到其量化操作：与传统的深度优先实现相比，采用嵌套扫描的Adiar能够解决更多问题，和/或更快地解决问题。

Keyword:

Time-forward Processing

External Memory Algorithms

Binary Decision Diagrams