3

次のブール関数があるとします。

or(x, y) := x || y
and(x, y) := x && y
not(x) := !x
foo(x, y, z) := and(x, or(y, z))
bar(x, y, z, a) := or(foo(x, y, z), not(a))
baz(x, y) := and(x, not(y))

ここで、それらから二分決定図を作成したいと思います。私はいくつかの論文を調べましたが、これらのようなネストされた論理式からそれらを構築する方法を見つけることができませんでした.

ブール関数は根付き有向非巡回グラフであると言われています。いくつかの非ターミナル ノードとターミナル ノードがあります。次に、各非終端ノードが、2 つの子ノードを持つブール変数(関数ではない) によってラベル付けされていることを示しています。上記の関数定義から、ブール変数が何であるかわかりません。ノードから子aまたはノードへのエッジは、それぞれノードの 0 または 1 への割り当てbを表します。同形サブグラフがマージされ、2 つの子が同形であるノードが削除された場合、縮小されたと呼ばれます。これは縮小順序二分決定図 (ROBDD) です。

それから、そして私が遭遇したすべてのリソースから、これらの関数をBDD/ROBDDに変換する方法を理解できませんでした:

foo(1, 0, 1)
bar(1, 0, 1, 0)
baz(1, 0)

あるいは、変換する必要があるのは次のようなものかもしれません:

foo(x, y, z)
bar(x, y, z, a)
baz(x, y)

これを根付き有向非循環グラフにするために何をする必要があるかについての説明を探しています。データ構造がどのように見えるかを知ることも役に立ちます。これだけのようです：

var nonterminal = {
  a: child,
  b: child,
  v: some variable, not sure what
}

しかし、問題は、これらの関数foo、bar、およびからグラフを構築する方法bazです。

4

3 に答える 3

2

基本的な論理演算 AND、OR、XOR などはすべて、BDD 表現の関数間で計算して、BDD 表現の新しい関数を生成できます。これらのアルゴリズムは、端末の処理方法を除けばすべて類似しており、大まかに次のようになります。

  • 結果が端末の場合、その端末を返します。
  • がキャッシュされている場合(op, A, B)は、キャッシュされた結果を返します。

  • 3つのケースを区別します（実際、これを一般化できます..）

    1. A.var == B.var、このプロシージャを再帰的に呼び出すことを表すノードを作成し(A.var, OP(A.lo, B.lo), OP(A.hi, B.hi))ます。OP
    2. A.var < B.var、ノードを作成します(A.var, OP(A.lo, B), OP(A.hi, B))
    3. A.var > B.var、ノードを作成します(B.var, OP(A, B.lo), OP(A, B.hi))
  • 結果をキャッシュする

「ノードの作成」はもちろん、「削減」要件を満たすために、それ自体を重複排除する必要があります。3 つのケースに分割することで、注文要件に対応できます。

単純な操作のツリーである複雑な関数は、BDD の単純な組み合わせのみを実行するたびに、このボトムアップを適用することによって BDD で変換できます。もちろん、これは最終結果の一部ではないノードを生成する傾向があります。変数と定数には自明な BDD があります。

たとえば、はそのツリーに深さ優先で進み、変数(自明なノード)and(x, or(y, z))の BDD を作成し、次にとを実行して作成されます (上記のアルゴリズムのインスタンスで、最初のステップだけが実際に演算はとを表すBDD に対して実行され、結果と変数を表す BDD に対して実行されます。正確な結果は、選択した変数の順序によって異なります。x(x, 0, 1)yzORORyzANDx

それ自体の内部で他の関数を評価する関数は、BDD で可能であるがいくつかの悪い最悪のケースがある関数合成 (既に BDD によって呼び出された関数を表す場合) を必要とするか、呼び出された関数の定義を単にインライン化する必要があります。

于 2018-05-29T23:17:12.587 に答える