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

Question

假设我有以下布尔函数：

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

现在我想从中构建一个 Binary Decision Diagram。我已经浏览了几篇论文，但一直无法找到如何从像这样的嵌套逻辑公式构造它们。

据说布尔函数是有根的、有向的、无环图。它有几个非终端节点和终端节点。然后它说每个非终端节点都由一个布尔变量（不是函数）标记，它有两个子节点。我不知道上面的函数定义中的布尔变量是什么。从节点到子节点a或b的一条边分别代表节点赋值为0或1。如果已合并同构子图，则称为reduced，并且删除两个子节点是同构的节点。这是一个降序二元决策图 (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.

构建图表

Answer 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
...

请注意，节点必须标有要在以下图形边上分配的变量名称。该算法不是很复杂（当然有更有效的算法），但我希望它能将策略可视化。

Answer 2

基本逻辑运算 AND、OR、XOR 等都可以在 BDD 表示的函数之间计算，以产生 BDD 表示的新函数。除了处理终端的方式外，这些算法都相似，大致如下：

如果结果是一个终端，return那个终端。
如果 (op, A, B) 被缓存，return 缓存的结果。
区分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))
缓存结果

"Create a node" 当然应该对自身进行重复数据删除，以满足 "reduced" 的要求。拆分为 3 种情况可满足排序要求。

作为简单操作树的复杂函数可以通过应用这个自下而上的方法在 BDD 中转换，每次只做 BDD 的简单组合。这当然会产生不属于最终结果的节点。变量和常量具有微不足道的 BDD。

例如，and(x, or(y, z)) 是通过深度优先进入该树创建的，为变量 x（一个普通节点，(x, 0, 1)）创建 BDD，然后为 y 和 z，在表示 y和z，然后对结果执行AND，BDD表示变量x。确切的结果取决于您选择的变量排序。

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

Answer 3

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

所描述的示例可以使用 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 语句生成）。

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

How to turn a Boolean Function into a Binary Decision Diagram

algorithm

data-structures

logic

graph-theory

binary-decision-diagram