问题描述
我正在尝试创建具有特定结构的 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