1

我正在尝试创建具有特定结构的 BDD。我有一个布尔变量 x_i 的一维序列，例如 x_1、x_2、x_3、x_4、x_5。如果没有孤立的一或零（可能在边缘除外），我的条件就满足了。

我已经使用pyeda实现了这一点，如下所示。该条件相当于检查连续的三元组 ([x_1, x_2, x_3]; [x_2, x_3, x_4]; ...) 并检查它们的真值是否为 [[1,1,1], [0, 0,0]，[1,1,0]，[0,1,1]，[1,0,0]，[0,0,1]]。

from functools import reduce
from pyeda.inter import bddvars

def possible_3_grams(farr):
    farr = list(farr)
    poss = [[1,1,1], [0,0,0], [1,1,0], [0,1,1], [1,0,0], [0,0,1]]
    truths = [[farr[i] if p[i] else ~farr[i] for i in range(3)] for p in poss]
    return reduce(lambda x, y: x | y, [reduce(lambda x, y: x & y, t) for t in truths])

X = bddvars('x', k)
Xc = [X[i-1:i+2] for i in range(1,k-1)]
cont_constraints = [possible_3_grams(c) for c in Xc]
cont_constr = reduce(lambda x, y: x & y, cont_constraints)
print(cont_constr.to_dot())

最终的图表如下所示：

BDD

这适用于短序列，但是当长度超过 25 时，最后的减少变得非常缓慢。我想要一些适用于更长序列的东西。

我想知道在这种情况下直接构建 BDD 是否更有效，因为问题有很多结构。但是，我找不到任何方法来直接在 pyeda 中操作 BDD。

有谁知道我怎样才能更有效地完成这项工作？

4

1 回答 1

1

这个例子可以解决大量的变量使用包dd，它可以安装

pip install dd

例如，

from functools import reduce

from dd.autoref import BDD


def possible_3_grams(farr):
    farr = list(farr)
    poss = [[1, 1, 1], [0, 0, 0], [1, 1, 0], [0, 1, 1], [1, 0, 0], [0, 0, 1]]
    truths = [[farr[i] if p[i] else ~ farr[i] for i in range(3)] for p in poss]
    return reduce(lambda x, y: x | y, [reduce(lambda x, y: x & y, t) for t in truths])


def main():
    k = 100
    xvars = [f'x{i}' for i in range(k)]
    bdd = BDD()
    bdd.declare(*xvars)
    X = [bdd.add_expr(x) for x in xvars]
    Xc = [X[i-1:i+2] for i in range(1, k-1)]
    cont_constraints = [possible_3_grams(c) for c in Xc]
    cont_constr = reduce(lambda x, y: x & y, cont_constraints)
    print(cont_constr)
    bdd.dump('example.png', [cont_constr])

以上使用模块中 BDD 的纯 Python 实现dd.autoref。模块中有一个可用的 Cython 实现，dd.cudd它与 C 中的 CUDD 库接口。可以通过替换 import 语句来使用此实现

from dd.autoref import BDD

与声明

from dd.cudd import BDD

使用该类的上述脚本dd.autoref.BDD适用于k = 800（带有bdd.dump注释的语句）。使用类的上述脚本dd.cudd.BDD适用于k = 10000，前提是首先禁用动态重新排序bdd.configure(reordering=False)，并构造一个具有 39992 个节点的 BDD（带有bdd.dump注释的语句）。

图表k = 100如下：

k=100 的 BDD 图

如果两级逻辑最小化也感兴趣，它在包中实现omega，可以在以下位置找到示例：https ://github.com/tulip-control/omega/blob/master/examples/minimal_formula_from_bdd.py

于 2021-01-10T12:57:51.737 回答