2

这个问题有点长；请多多包涵。

我有一个包含如下元素的数据结构{x1, x2, x3, x4, x5}：

{0 0 0 0 0, 0 0 0 1 0, 1 1 1 1 0,.....}

它们代表真值表中的所有 TRUE。当然，该集合中不存在的 5 位字符串元素对应于真值表中的 FALSE。但是我没有对应于所述集合数据结构的布尔函数。

我看到了这个问题，但这里所有的答案都假设给出了布尔函数，这是不正确的。

我需要构建一个 ROBDD，然后从给定的数据结构到 ZDD。最好使用这些可用的 python 包。

专家有什么建议吗？我确信在这方面已经做了很多工作。

4

1 回答 1

4

使用可以使用包管理器安装的 Python 包dd，可以将布尔函数所在的变量赋值集转换为二元决策图。pippip install ddTRUE

Python 中的以下示例假定函数的赋值是TRUE作为一组字符串给出的。

from dd import autoref as _bdd


# assignments where the Boolean function is TRUE
data = {'0 0 0 0 0', '0 0 0 1 0', '1 1 1 1 0'}

# variable names
vrs = [f'x{i}' for i in range(1, 6)]
# convert the assignments to dictionaries
assignments = list()
for e in data:
    tpl = e.split()
    assignment = {k: bool(int(v)) for k, v in zip(vrs, tpl)}
    assignments.append(assignment)

# initialize a BDD manager
bdd = _bdd.BDD()
# declare variables
bdd.declare(*vrs)
# create binary decision diagram
u = bdd.false
for assignment in assignments:
    u |= bdd.cube(assignment)

# to confirm
satisfying_assignments = list(bdd.pick_iter(u))
print(satisfying_assignments)

为了更快地实现 BDD，以及使用 C 库CUDDdd.cudd实现 ZDD ，Cython 模块扩展dd.cudd_zdd可以按如下方式安装：

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

dd.autoref对于这个（小）示例，纯 Python 模块和 Cython 模块之间没有实际的速度差异dd.cudd。

上面的二元决策图 (BDD)可以使用以下代码复制到零抑制二元决策图 (ZDD) ：

from dd import _copy
from dd import cudd_zdd


# initialize a ZDD manager
zdd = cudd_zdd.ZDD()
# declare variables
zdd.declare(*vrs)
# copy the BDD to a ZDD
u_zdd = _copy.copy_bdd(u, zdd)

# confirm
satisfying_assignments = list(zdd.pick_iter(u_zdd))
print(satisfying_assignments)

该模块dd.cudd_zdd已添加dd == 0.5.6，因此上述安装需要dd >= 0.5.6从PyPI或GitHub 存储库下载分发包。

于 2020-05-12T17:02:08.827 回答