Zusammensetzung von ROBDD

Question

Ich versuche zu verstehen, wie die Zusammensetzung von zwei ROBDDs funktioniert.

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

Ich brauche eine Formel F3 zu finden, die durch Ersetzen Sie alle Vorkommen von d durch Formel F1 in Formel F2 erhalten wird.

Wie gehe ich fort, das zu lösen?

Answer 1

Substitution, Zusammensetzung von BDDs, Variable Umbenennung, Cofaktoren und Auswertung sind all the same mathematische Operation: Substitution. Sie können die Substitution tun, sind Sie daran interessiert, die Python package dd bei der Verwendung wie folgt:

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

Die oben erzeugt die Ausgabe:

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

und die Datei foo.png weiter unten. Für Zuordnungen von Booleschen Werten zu den Variablen:

• f1_formula entspricht den negierten BDD am Knoten 7
• f2_formula am Knoten 14
• r (die Zusammensetzung) entspricht den BDD entspricht den BDD am Knoten 11
.

die "let" Methode wird nach dem LET... IN benannt konstruieren in TLA+.