ROBDD의 구성

Question

두 ROBDD의 구성이 어떻게 작동하는지 이해하려고합니다.

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

나는 공식 F2에 공식 F1으로 d의 모든 항목을 대체하여 얻어지는 식 F3을 찾을 필요가있다.

어떻게 해결할 수 있습니까?

Answer 1

대체, BDD 구성, 변수 이름 바꾸기, 보조 요소 및 평가는 all the same 수학 연산 : 대체입니다.

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 노드에 BDD 14
• r (조성물)를 대응 노드 (11)에 BDD에 대응하는 노드에서 부정 BDD에 대응 .

은 "하자"방법은 LET... IN의 이름을 따서 명명된다 TLA+에 건설하십시오.