使用 CUDD/DDDMP 包将 BDD 存储在文件中?

Question

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

Answer 1

DDDMP 包的接口可通过 Python 包的 CUDD 的 Cython 绑定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.cudd安装dd，可以总结为

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

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