algorithm - 由ROBDD组成

我试图了解两个机器人的组成是如何工作的。

F1 = (d? false: (c? (a? false: true): false))
F2 = (d? (b? true: (a? false: true)): (c? (b? true: (a? false: true)): true))

我需要找到一个公式F3，用公式d中的公式F1替换所有出现的F2。
我该如何解决这个问题？

最佳答案

替换、bdd的组成、变量重命名、辅助因子和求值都是all the same数学运算：替换。您可以使用Python package dd进行您感兴趣的替换，如下所示：

from dd import autoref as _bdd


f1_formula = 'ite(d, FALSE, ite(c, ite(a, FALSE, TRUE), FALSE))'
f2_formula = (
    'ite(d, ite(b, TRUE, ite(a, FALSE, TRUE)), '
    'ite(c, ite(b, TRUE, ite(a, FALSE, TRUE)), TRUE))')
# create a BDD manager and BDDs for the above formulas
bdd = _bdd.BDD()
bdd.declare('a', 'b', 'c', 'd')
f1 = bdd.add_expr(f1_formula)
f2 = bdd.add_expr(f2_formula)
# substitute `f1` for `d` in `f2`
sub = dict(d=f1)
r = bdd.let(sub, f2)
# dump the BDDs to a PNG file
bdd.dump('foo.png', [f1, f2, r])
print('f1: {f1}, f2: {f2}, r: {r}'.format(f1=f1, f2=f2, r=r))

以上创建输出：

f1: @-7, f2: @14, r: @11

文件foo.png如下所示。对于变量的布尔值赋值：
f1_formula对应于节点7处的取反bdd
f2_formula对应于节点14处的bdd
r（构图）对应于节点11处的bdd。

“let”方法以TLA+中的LET... IN结构命名。

关于algorithm - 由ROBDD组成，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/44032511/