binary-decision-diagram - 使用 CUDD/DDDMP 包将 BDD 存储在文件中？

Question

我已经使用 CUDD 包成功创建了 BDD。我还可以使用一些已经构建的工具对其进行可视化。我有兴趣使用 CUDD 的 DDDMP 包将 BDD 存储在文件中。我读到Dddmp_cuddBddStore()正在为我们做这件事。我找不到使用该功能的任何示例。它的论点有点复杂。任何使用该功能的小例子都会有很大帮助。

Answer 1

与 Python 包的 CUDD 的 Cython 绑定提供了 DDDMP 包的接口dd。下面是一个创建布尔函数的 BDD，将其保存到 DDDMP 文件，然后从该文件加载它的示例。

from dd import cudd as _bdd

bdd = _bdd.BDD()
bdd.declare('x', 'y')

# The BDD node for the conjunction of variables x and y
u = bdd.add_expr('x /\ y')

# save to a DDDMP file (the file extension matters,
# for example a PDF extension would result in plotting
# a diagram using GraphViz)
bdd.dump('storage.dddmp', [u])

# load the BDD from the DDDMP file
u_ = bdd.load('storage.dddmp')
assert u == u_, (u, u_)

Cython 模块的源代码dd/cudd.pyx包括如何使用函数的示例Dddmp_cuddBddStore和Dddmp_cuddBddLoad

https://github.com/tulip-control/dd/blob/b625dd46120e2e1f5a12190332e6191d07681ee8/dd/cudd.pyx#L1157-L1222

这里描述dd了使用模块的安装，可以总结为dd.cudd

pip download dd --no-deps
tar -xzf dd-*.tar.gz
cd dd-*/
python setup.py install --fetch --cudd

这将下载和构建 CUDD，并构建和安装到 CUDD 的 Cython 绑定dd。