高效创建结构化二元决策图

Question

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

我已经使用pyeda实现了这一点，如下所示。该条件等效于检查连续的三元组(x_1，x_2，x_3；x_2，x_3，x_4；...)并检查它们的真值是否为[1, 1, 1，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())

最终的图表如下所示：

​

​

这对于短序列很有效，但当长度超过约25时，最后一次缩减会变得非常慢。我想要一些更长序列的东西。

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

有没有人知道我怎样才能更有效地工作？

Answer 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])

上面的代码在模块dd.autoref中使用了BDDs的纯Python实现。在模块dd.cudd中有一个Cython实现，它连接到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.configure(reordering=False)(带有注释的bdd.dump语句)。

k = 100的图表如下所示：

​

​

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