我想了解两个 ROBDD 的组合是如何工作的。
F1 = (d? false: (c? (a? false: true): false))
F2 = (d? (b? true: (a? false: true)): (c? (b? true: (a? false: true)): true))
我需要找到一个公式F3
,它是通过用公式F2<中的公式
。 F1
替换所有出现的d
获得的
我该如何继续解决这个问题?
最佳答案
替换、BDD 的组成、变量重命名、辅助因子和评估是 all the same数学运算:代入。您可以使用 Python package dd
进行您感兴趣的替换。如下:
import dd.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(f'f1: {f1}, f2: {f2}, r: {r}')
以上创建输出:
f1: @-7, f2: @14, r: @11
和如下所示的文件 foo.png
。对于将 bool 值赋值给变量:
f1_formula
对应节点 7 的取反 BDDf2_formula
对应节点14处的BDDr
(组合)对应节点 11 处的 BDD。
“let”方法以 TLA+ 中的 LET...IN
结构命名。 .
关于algorithm - ROBDD的组成,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/44032511/