Composition de ROBDD

Question

J'essaie de comprendre comment fonctionne la composition de deux ROBDD.

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

Je dois trouver une formule F3 qui est obtenue en remplaçant toutes les occurrences de d par la formule F1 dans la formule F2.

Comment résoudre ce problème?

Answer 1

Substitution, composition de BDD, changement de nom, cofacteurs et évaluation sont all the same opération mathématique: substitution. Vous pouvez faire la substitution que vous êtes intéressé à utiliser le Python package dd comme suit:

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

Le crée au-dessus de la sortie:

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

et le fichier foo.png illustré ci-dessous. Pour les affectations de valeurs booléennes à des variables:

• f1_formula correspond à la BDD réduit à néant au noeud 7
• f2_formula correspond à la BDD au noeud 14
• r (la composition) correspond à la BDD au noeud 11 .

la méthode "let" porte le nom du LET... IN construire en TLA+.