가방 모델을 사용하여 발생 비트가 포함 된 BDD를 작성하는 방법

Question

라이센스가있는 안내서를 통해 가방을 모델로 사용하여 BDD를 산출하는 가방 모델로 제품 패밀리를 나타 냈습니다.

내 단계에 비슷한 단계를 포함하려고합니다. 텍스트에

우리가 가방 모델을 채택하면 구현은 기능의 복제를 제외하고 세트 모델 구현과 유사합니다. ROBDD는 노드의 중복을 허용하지 않습니다. BDD 자체 내의 기능 발생 횟수를 처리하기 위해 인코딩 수준 인 을 고안했습니다. 이 숫자 바이너리를 인코딩합니다. 예를 들어 x, y, z의 3 가지 기능을 가진 제품이 있고 기능의 최대 발생 횟수가 인 경우 인코딩하려면 3 개의 2 진 비트가 필요합니다. 제품군 W에 3 개의 x 피처와 6 개의 z 피쳐 및 0 개의 y 피처가있는 제품이 하나 있다고 가정하십시오. 우리 제품군에는 그림 3.7에 BDD 으로 표시된 제품 Pt가 들어 있습니다. 이 가방을 나타내는 BDD는 세트 모델과 유사한 방식으로 제품을 설명합니다. 그러나 bl, b2 및 b3을 포함하는 노드 수준에서 발생을 인코딩합니다. 그림 3.7에서 x가이 제품에 존재하면 은 bl과 b2를 선택해야하지만 b3은 선택하지 않아야합니다. 이것은 각각 x에 대해 3의 발생을 나타내는 b3, b2 및 bl을 나타내는 이진 코드 011입니다. 마찬가지로 y가이 제품에 존재할 경우 이진 발생 인코딩이 000이되고 0 번 발생합니다. z의 경우, 이진수 110이 6이라는 숫자를 갖습니다. >

- 이로써 그래서

하는 제품군 Z = 대해 {{(X, 3), (Y, 0), (Z는, 6)}} 대응 BDD는 것 제품의 가족 W에 대한

= {{(X는, 3), (Y, 1), (Z는 7)}}는 BDD는

것 그러나 그가 어떻게 마련 않았다 이러한 BDD에는 BDD의 기본 공식이 있어야합니다. 주어진 가족을위한 동일한 공식에 어떻게 도달하는지 이해하도록 도와 주시겠습니까? 그렇기 때문에 다른 사용 사례에서도 마찬가지로 사용할 수 있습니다. 감사.

Answer 1

bag은 여러 번 발생하는 요소의 모음입니다. Temporal Logic of Actions (TLA+)에있는 표준 모듈 Bags에는 bag에 해당하는 수학적 정의가 들어 있습니다.

binary decision diagram의 그래프를 수식으로 변환하려면 아래 코드를 사용하십시오. OP의 첫 번째 BDD에 대한 대답은 다음과 같습니다.

/\ b \in 0 .. 7 
/\ x \in 0 .. 1 
/\ y \in 0 .. 1 
/\ z \in 0 .. 1 
/\ \/ (b = 0) /\ (y = 1) 
    \/ (b = 3) /\ (x = 1) 
    \/ (b = 6) /\ (z = 1) 

이 표현식은 TLA +로 작성되었습니다. y를 생략하는 것은 BDD에 대응로 돌려한다 가방 각 요소 (들 중 적어도 하나 개를 발생하는 것을 포함하고 있기 때문에

는

상기 실제로 그래서 y 전혀 발생 이것이 가방 없다는 것을 의미하지 가방 아니다 가방). 가방이 제품군에 적합한 표현인지 여부는 별도의 관심사이며, 여기서는 다루지 않을 것입니다.

코드를 적용하여 두 번째 그림에 표시된 BDD에 대한 수식을 확인할 수 있습니다.

아래 코드는 Python 패키지 omega == 0.1.1과 dd == 0.5.1 (면책 조항 : 나는 이들의 작성자입니다)을 사용합니다. 이것들은 순수 Python에서 작동합니다.이 크기의 BDD 만 있으면 충분합니다 (그렇지 않으면 dd.cudd을 작성하면 CUDD을 사용할 수 있습니다. 물론 손으로 쓸 수있는 BDD의 경우에는 아무런 차이가 없습니다).

#!/usr/bin/env python 
"""Convert from a BDD figure to a formula.""" 
from omega.symbolic import fol 

# "bare" BDDs (without integers) can be used also 
# via the package `dd` 
# from dd import autoref as _bdd 

# bdd = _bdd.BDD() 

ctx = fol.Context() 
ctx.declare(x=(0, 1), y=(0, 1), z=(0, 1), b=(0, 7)) 

bdd = ctx.bdd 
# bdd.declare('x', 'y', 'z', 'b1', 'b2', 'b3') 

# level of b3 
u1 = bdd.add_expr('b_2') 
u2 = bdd.add_expr('~ b_2') 
# level of b2 
u3 = bdd.add_expr('ite(b_1, {u}, False)'.format(u=u1)) 
u4 = bdd.add_expr('ite(b_1, False, {u})'.format(u=u2)) 
u5 = bdd.add_expr('ite(b_1, {u1}, {u2})'.format(u1=u1, u2=u2)) 
u6 = bdd.add_expr('ite(b_1, {u2}, False)'.format(u2=u2)) 
# level of b1 
u7 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
    low=u3, high='False')) 
u8 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
    low=u4, high='False')) 
u9 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
    low=u5, high='False')) 
u10 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
    low=u3, high=u6)) 
u11 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
    low='False', high=u6)) 
u12 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
    low=u4, high=u6)) 
u13 = bdd.add_expr('ite(b_0, {high}, {low})'.format(
    low=u5, high=u6)) 
# level of z 
u14 = bdd.add_expr('ite(z_0, {high}, {low})'.format(
    low='False', high=u7)) 
u15 = bdd.add_expr('ite(z_0, {high}, {low})'.format(
    low=u8, high=u9)) 
u16 = bdd.add_expr('ite(z_0, {high}, {low})'.format(
    low=u11, high=u10)) 
u17 = bdd.add_expr('ite(z_0, {high}, {low})'.format(
    low=u12, high=u13)) 
# level of y 
u18 = bdd.add_expr('ite(y_0, {high}, {low})'.format(
    low=u14, high=u15)) 
u19 = bdd.add_expr('ite(y_0, {high}, {low})'.format(
    low=u16, high=u17)) 
# level of x 
from_fig = bdd.add_expr('ite(x_0, {high}, {low})'.format(
    low=u18, high=u19)) 

# the variable order from the first figure in the OP 
levels = dict(x_0=0, y_0=1, z_0=2, b_0=3, b_1=4, b_2=5) 
fol._bdd.reorder(bdd, levels) 
bdd.dump('foo_1.png', [from_fig]) 
# a better variable order 
levels = dict(b_0=0, b_1=1, b_2=2, x_0=3, y_0=4, z_0=5) 
fol._bdd.reorder(bdd, levels) 
bdd.dump('foo_2.png', [from_fig]) 

# Create the BDD directly from an expression 
s = ''' 
    \/ (b = 3 /\ x = 1) 
    \/ (b = 0 /\ y = 1) 
    \/ (b = 6 /\ z = 1) 
    ''' 
from_formula = ctx.add_expr(s) 
assert from_formula == from_fig 

# print a minimal formula in disjunctive normal form 
# use this to covert BDDs to expressions 
print(ctx.to_expr(from_fig, show_dom=True)) 

종속성

는 pip 함께 설치 될 수있다 : 위의 코드에서 수행 같은 변수의 수치를 재정렬함으로써

pip install dd==0.5.1 
pip install omega==0.1.1 

, 우리는 더 작은 (RO) BDD를 얻을 수있다 :

위의 BDD는 negated edges을 사용하여 표현되며, 이에 대해서는 tutorial on BDDs에서 설명합니다.