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

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

我正在尝试创建具有特定结构的 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]]。

from functools import reduce
from pyeda.inter import bddvars

def possible_3_grams(farr):
    farr = list(farr)
    poss = [[1,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,cont_constraints)
print(cont_constr.to_dot())

最终的图表如下所示：

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

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

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

解决方法

这个例子可以使用包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],[1,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 = ['x{i}'.format(i=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,cont_constraints)
    print(cont_constr)
    bdd.dump('example.png',[cont_constr])

以上使用模块dd.autoref中BDD的纯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（注释了 bdd.dump 语句）。

k = 100 的示意图如下：

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