ROBDDの構成

Question

2つのROBDDの構成の仕組みを理解しようとしています。

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

Iは式F2式F1でdのすべての出現を置き換えたものである式F3を見つける必要があります。

どうすれば解決できますか？

Answer 1

置換、BDDの構成、変数の名前変更、補因子および評価は、数学演算：代入です。

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あなたは次のようにPython package ddを使用することに興味を持っている置換を行うことができます。変数へのブール値の割り当てのために：

• f1_formulaノード7
• f2_formulaノード14
• rにおけるBDD（組成物）は、ノード11でのBDDに対応するに対応するでネゲートBDDに対応します。

"せ" 方法はLET... INにちなんで命名されましたTLA+に建設してください。