バッグモデルを使用して発生ビットを含むBDDを作成する方法

Question

私は、製品ファミリをバッグモデルとして表現するためのガイドを行っていました。このモデルでは、発生を考慮してBDDが発生します。

私は私の問題に同様の手順を含めることを試みています。テキストは

と言っています。バッグモデルを採用すると、実装は機能の複製を処理する以外はセットモデルの実装と似ています。 ROBDDはノードの重複を許可しません。 BDD内でのフィーチャの発生回数を処理するために、それをエンコードする発生レベルを と考案しました。この数値バイナリをエンコードします。たとえば、x、y、zという3つのフィーチャを持つ製品があり、フィーチャの最大発生数がの場合、エンコーディングには3つのバイナリビットが必要です。製品ファミリWに3つのxフィーチャと6つのzフィーチャとゼロのyフィーチャを持つ 製品が1つあります。当社の製品ファミリには、図3.7のBDD で表される製品Ptが含まれています。このバッグを表すBDDは、セットモデルと同様の方法で製品を記述します。ただし、bl、b2、およびb3を含むノードのレベルでは、 のオカレンスがエンコードされます。図3.7では、xがこの製品に存在する場合、 はb1とb2を選択する必要がありますが、b3は選択しないといけません。これは、 xに対して3の出現をそれぞれ有するb3、b2およびb1を表すバイナリコード011である。同様に、yがこの製品に存在するためには、バイナリオカレンス符号化が000である0オカレンスになります。 zについては、 のバイナリオカレンス110が得られます。 >

- 製品ファミリー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には、バッグに対応する数学的定義が含まれています。

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 +で書かれています。

上記実際袋は、各要素の少なくとも1つの存在を含んでいるので、バッグない（そうyのない発生は、これは袋ではないことを意味し; yがに対応するBDDにそれを回す必要があり省略しますバッグ）。バッグが製品ファミリーに適したものであるかどうかは別の懸念事項です。

あなたは2番目の図に示したBDDのための式を確認するためのコードを適応させることができます。

以下のコードでは、Pythonパッケージomega == 0.1.1とdd == 0.5.1（免責事項：私はそれらの著者です）を使用しています。これらは、純粋なPythonで動作します。このサイズのBDDの場合は十分です（そうでなければ、dd.cuddをビルドするとCUDDを使用できます。もちろん手書きで書くには十分小さいBDDでは違いはありません）。依存関係がpipでインストールすることができる

#!/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 install dd==0.5.1 
pip install omega==0.1.1 

上記のコードで行われたように、変数のレベルを並べ替えることにより、我々は小さい（RO）BDDを得ることができます

上記のBDDはnegated edgesで表され、これはtutorial on BDDsで説明されています。