如何将布尔函数转换为二叉决策图

Question

如何将布尔函数转换为二叉决策图

algorithmdata-structureslogicgraph-theorybinary-decision-diagram

3

假设我有以下布尔函数：

or(x, y) := x || y
and(x, y) := x && y
not(x) := !x
foo(x, y, z) := and(x, or(y, z))
bar(x, y, z, a) := or(foo(x, y, z), not(a))
baz(x, y) := and(x, not(y))

现在我想从它们中构建一个二叉决策图。我查阅了几篇论文，但没有找到如何从这些嵌套逻辑公式中构建它们的方法。

据说布尔函数是一个根据方向的无环图。它有几个非终端和终端节点。然后它说每个非终端节点由布尔变量（而不是函数）标记，它有两个子节点。从节点到子节点a或b的边分别表示将节点分配为0或1。如果同构子图已合并，则称其为约简，并且删除其两个子节点是同构的节点。这是一个约简有序二叉决策图（ROBDD）。

从那里以及我遇到的所有资源中，我都无法弄清楚如何将这些函数转换为BDDs/ROBDDs：

foo(1, 0, 1)
bar(1, 0, 1, 0)
baz(1, 0)

或许需要转换的是这些：

foo(x, y, z)
bar(x, y, z, a)
baz(x, y)

我希望能得到关于如何将这个转换成根据方向有序且无环的图的解释。了解数据结构的样子也会很有帮助。看起来它只是这样的：

var nonterminal = {
  a: child,
  b: child,
  v: some variable, not sure what
}

但问题在于如何从这些函数foo、bar和baz构建图形。

- Lance

3个回答

1

你可以通过评估所有变量赋值来实现，例如在某些情况下。

foo(0,0,0) = 0
foo(0,0,1) = 0
foo(0,1,0) = 0
...

然后创建图表，从根开始。每个函数参数都会得到一个标有其赋值的边缘，叶节点则会标记结果值：

x0 -0-> y0 -0-> z0 -0-> 0
x0 -0-> y1 -0-> z1 -1-> 0
x0 -0-> y2 -1-> z2 -0-> 0
...

合并节点（y0 = y1 = y2，z0 = z1）：

x0 -0-> y0 -0-> z0 -0-> 0
x0 -0-> y0 -0-> z0 -1-> 0
x0 -0-> y0 -1-> z1 -0-> 0
...

减少节点（有一些规则可以允许合并节点或跳过节点）。例如，由于从根节点开始的0总是导致叶子节点0，因此您可以跳过后续的决策：

x0 -0-> 0
...

请注意，节点必须用变量名称标记，以便在以下图形边缘上分配。该算法并不是非常复杂（肯定存在更有效的算法），但我希望它能可视化策略。

- CoronA

你是在说必须预先计算所有函数的值吗？ - Lance

看到树的结构可能会很有帮助，例如采用 x1(x2(...)) 或者 var top = { data: ..., child1: ..., child2: ... } 这样的注释来表示。不太确定你所描述的结构是什么样子的。 - Lance

0

用于存储BDD的数据结构可以基于三元组(level, u, v)，其中u是当level处的变量为FALSE时布尔函数的节点，v是当level处的变量为TRUE时布尔函数的节点。

所描述的示例可以使用Python包dd进行编程（使用pip install dd安装纯Python实现）。代码如下：

from dd import autoref as _bdd

bdd = _bdd.BDD()
bdd.declare('x', 'y', 'z', 'a')
x_or_y = bdd.add_expr(r'x \/ y')
x_and_y = bdd.add_expr(r'x /\ y')
not_x = bdd.add_expr('~ x')

# variable renaming: x to y, y to z
let = dict(x='y', y='z')
y_or_z = bdd.let(let, x_or_y)

# using the method `BDD.apply`
foo = bdd.apply('and', bdd.var('x'), y_or_z)

# using a formula
foo_ = bdd.add_expr(r'x /\ (y \/ z)')
assert foo == foo_

# using the string representation of BDD node references
foo_ = bdd.add_expr(rf'x /\ {y_or_z}')
assert foo == foo_

bar = bdd.apply('or', foo, ~ bdd.var('a'))
bar_ = bdd.add_expr(rf'{foo} \/ ~ a')

assert bar == bar_

let = dict(y= ~ bdd.var('y'))
baz = bdd.let(let, x_and_y)
baz_ = bdd.add_expr(r'x /\ ~ y')
assert baz == baz_
# plotting of the diagram using GraphViz
bdd.dump('foo.png', [foo])

这个例子包括了在BDD之间直接应用运算符（使用方法BDD.apply或解析调用这些运算符的布尔公式）以及将函数表示为BDD进行函数组合（使用方法BDD.let重命名变量和替换变量的BDD，以及语法f'{u}'用于对BDD节点引用的字符串表示）。

绘制布尔函数foo的结果如下所示（由上述代码中的bdd.dump语句生成）。

- 0 _

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- harold · Accepted Answer

基本的逻辑运算AND、OR、XOR等都可以在BDD表示法中计算函数之间，得出一个新的BDD表示法的函数。这些算法都很相似，除了它们如何处理终端之外，大致流程如下：

- 如果结果是终端，则返回该终端。 - 如果(op, A, B)已经缓存，则返回缓存结果。 - 区分3种情况（实际上你可以将其概括为...） 1. A.var == B.var，创建一个节点(A.var, OP(A.lo, B.lo), OP(A.hi, B.hi))，其中OP代表递归调用此过程。 2. A.var < B.var，创建一个节点(A.var, OP(A.lo, B), OP(A.hi, B)) 3. A.var > B.var，创建一个节点(B.var, OP(A, B.lo), OP(A, B.hi)) - 缓存结果

“创建一个节点”当然要去重，以满足“减少”要求。在3个情况中的分割考虑到了排序要求。

由简单操作组成的树形复杂函数可以通过从底向上应用此方法来转换成BDD，在每一步只对BDD进行简单组合。当然，这样做确实会生成不属于最终结果的节点。变量和常数有平凡的BDD。

例如，and(x, or(y, z))是通过深度优先进入该树，为变量x创建一个BDD（一个平凡的节点(x, 0, 1)），然后为y和z创建BDD，对表示y和z的BDD执行OR（上述算法的实例，其中只有第一步真正关心操作是OR），然后对结果和表示变量x的BDD执行AND。确切的结果取决于您选择的变量顺序。

在自身内部评估其他函数的函数需要函数组合（如果已经用BDD表示被调用的函数）这在BDD中是可行的，但最坏情况很糟糕，或者只需内联调用函数的定义。