algorithm - BDD で表される関係における一意のタプルの拡張検索

Question

{<1,2>, <1,3>, <1,7>, <0,4>} をリレーション R のタプルの集合と考えてください。ここで、R が (そのメンバーシップ関数を介して) BDD。つまり、R を表す BDD は変数 {x1,x2, y1, y2, y3} に依存します。ここで、{x1, x2} はすべてのタプルの最初の要素を表すために使用され、{y1, y2, y3} はタプルを表すために使用されます。 2 番目の要素。

ここで、最初の要素に一意の値を持つタプルのセットを見つける問題を考えてみましょう。上記の関係の場合、そのセットは {<0,4>} になります。他のすべての要素は、最初のコンポーネントに 1 を持つ複数の値であるため、破棄されます。

2 番目の例として、タプルのセット {<1,2>, <1,3>, <1,7>, <2,3>, <2,5>, <0,4>} との関係を考えます。このような場合、最初の要素として 2 が複数回出現するため、期待される結果は依然として {<0,4>} です。

この問題は、変数 {y1,y2,y3} を抽象化して、{x1,x2} の一意の値のみが残るようにすることとも見なすことができます。この結果を使用して、結果のBDDと入力BDDの結合を計算することにより、期待される関係を再構築できます。

要約すると、問題は次のとおりです。一意のタプルのみで BDD を取得するために R の表現に対して実行する必要がある BDD 操作はどれですか。

これはこの質問の一般化であることに注意してください

編集 1: 次のコードは、これまでの実装を反映しています。ただし、より効率的なバージョンを入手できるかどうかは疑問です。簡単にするために、計算されたテーブルの処理を意図的に省略しています (時間の複雑さを改善するために重要です)。さらに、 &, | を使用します。と！BDD の論理積、論理和、補数の操作を表す。

BDD uniqueAbstract(BDD f, BDD cube) {
  if ((f.IsZero() || f.IsOne()) && !cube.IsOne())
    return zero();
  BDD T = high(f);
  BDD E = low(f);
  if(level(f) == level(c)) { // current var is abstracted
    BDD uniqueThen = uniqueAbstract(T, high(c));
    BDD existElse = existAbstract(E, high(c));

    BDD existThen = existAbstract(T, high(c));
    BDD uniqueElse = uniqueAbstract(E, high(c));

    return (uniqueThen & !existElse) | (uniqueElse & !existThen)
  } else {
    BDD uniqueThen = uniqueAbstract(T,c);
    BDD uniqueElse = uniqueAbstract(E,c);
    return ite(top(f), uniqueThen, uniqueElse);
  }
}

EDIT2: 3 つの異なる実装を試した後、まだパフォーマンスの問題がいくつかあります。その3つについて説明します。

私のアプローチの AC 実装、参照実装4と呼ばせてください。
受け入れられた回答3でユーザー meolic によって提案された実装。
2 つの利用可能なハイブリッドアプローチ2。

この更新の目的は、3 つのアプローチを使用した結果を少し分析することです。現時点では、時間測定はそれらを判断するのに誤解を招くように思われるため、別の一連の測定で実装を評価することにしました。

再帰呼び出し
キャッシュヒット
抽象的なシンプル。存在の抽象化を必要とせずに関数呼び出しが解決された回数。
抽象複合: 存在する抽象化を必要とする関数呼び出しが解決された回数。
Exist abstract: 存在抽象化への呼び出しの数。

実装 1 の結果: (21123 ミリ秒): 一意の抽象統計: 再帰呼び出し: 1728549.000000 キャッシュヒット: 638745.000000 非抽象: 67207.000000 単純な抽象: 0.000000 複雑な抽象: 0.000000

実装 2 の結果: (実行時間: 54727 ミリ秒) 一意の抽象統計: 再帰呼び出し: 191585.000000 キャッシュヒット: 26494.000000

実装 3 の結果: (実行時間: 20215 ミリ秒) 固有の抽象統計: 再帰呼び出し: 268044.000000 キャッシュヒット: 30668.000000

EDIT 3: ITE 5に関してすべての論理演算を実装した後、次の結果が得られました。

uniqueAbstractRecRef (21831 ミリ秒) 一意の抽象化統計: 呼び出しの総数: 1723239 最適化された呼び出し: 0 存在する抽象呼び出しの総数: 30955618 存在する抽象への一意の抽象呼び出し: 2385915 ite 呼び出しの総数: 3574555
uniqueAbstractSERec (56761 ミリ秒) 一意の抽象化統計: 呼び出しの総数: 193627 最適化された呼び出し: 60632 存在する抽象呼び出しの総数: 16475806
uniqueAbstractRec (20587 ミリ秒) 一意の抽象化統計: 呼び出しの総数: 270205 最適化された呼び出し: 78486 存在する抽象呼び出しの総数: 13186348

score 2 · Accepted Answer

これが私の実装です。私は著者が提案したソリューションを研究しましたが、任意の順序付けのための唯一の単純な BDD ベースのソリューションではないにしても、それが最善であるように思えます。ただし、アルゴリズムが私の方法で実装されている場合、いくつかの改善があるかもしれません-確認してください. BDD パッケージに独自のラッパーを使用していますが、理解するのに問題はありません。

編集: 解決策を簡略化しました。関数 Bdd_GetVariableChar() は使用されなくなりました。

/* TESTING SOLUTION FOR QUESTION ON STACK OVERFLOW */
/* bdd_termFalse,bdd_termTrue: Boolean constants */
/* Bdd_isTerminal(f): check if f is Boolean constant */
/* Bdd_Low(f),Bdd_High(f): 'else' and 'then' subfunction */
/* Bdd_Top(f): literal function representing topvar of f */
/* Bdd_IsSmaller(f,g): check if topvar of f is above topvar of g */
/* existentialAbstraction(f,cube): \exist v.f for all v in cube */

Bdd_Edge specialAbstraction(Bdd_Edge f, Bdd_Edge cube) {
  if (Bdd_isTerminal(cube)) return f;
  if (Bdd_isTerminal(f)) return bdd_termFalse;
  if (Bdd_IsSmaller(f,cube)) {
    Bdd_Edge E,T;
    E = specialAbstraction(Bdd_Low(f),cube);
    T = specialAbstraction(Bdd_High(f),cube);
    return Bdd_ITE(Bdd_Top(f),T,E);
  } else if (Bdd_IsSmaller(cube,f)) {
    return bdd_termFalse;
  } else {
    Bdd_Edge E,T;
    cube = Bdd_High(cube);
    E = Bdd_Low(f);
    T = Bdd_High(f);
    if (Bdd_isEqv(E,bdd_termFalse)) {
      return specialAbstraction(T,cube);
    } else if (Bdd_isEqv(T,bdd_termFalse)) {
      return specialAbstraction(E,cube);
    } else {
      Bdd_Edge EX,TX,R;
      EX = existentialAbstraction(E,cube);
      TX = existentialAbstraction(T,cube);
      if (Bdd_isEqv(EX,TX)) return bdd_termFalse;
      R = Bdd_ITE(Bdd_ITE(EX,bdd_termFalse,T),
                  bdd_termTrue,
                  Bdd_ITE(TX,bdd_termFalse,E));
      return specialAbstraction(R,cube);
    }
  }
}

そして、はい、y の上の x で変数の順序付けが固定されている場合、アルゴリズムは実際にははるかに効率的になります。最も複雑な「else」ブロックからすべての計算を削除して、0 を返すだけです。

いくつかのテスト実行を次に示します。

CUBE (JUST IN CASE YOU ARE NOT FAMILIAR WITH BDD ALGORITHMS)
  +  y1 y2 y3 y4 y5

ORIGINAL (ORDERED WITH X ABOVE Y)
  +  *x1 *x2 x3 *x4 x5 y1 *y2 y3 y4 y5
  +  *x1 x2 *x3 *x4 *x5 y1 y2 *y3 y4 y5
  +  *x1 x2 *x3 *x4 x5 *y1 y2 *y3 y4 y5
  +  *x1 x2 *x3 x4 *x5 y1 *y2 y3 *y4 *y5
  +  *x1 x2 x3 *x4 x5 *y1 *y2 *y3 *y4 y5
  +  *x1 x2 x3 *x4 x5 *y1 y2 y3 *y4 *y5
  +  x1 *x2 *x3 *x4 *x5 y1 y2 y3 y4 *y5
  +  x1 x2 *x3 x4 x5 *y1 *y2 *y4 *y5
  +  x1 x2 x3 *x4 *x5 *y1 *y2 *y3 y4 *y5

ABSTRACTION
  +  *x1 *x2 x3 *x4 x5
  +  *x1 x2 *x3 *x4
  +  *x1 x2 *x3 x4 *x5
  +  x1 *x2 *x3 *x4 *x5
  +  x1 x2 x3 *x4 *x5

ORIGINAL (ORDERED WITH Y ABOVE X)
  +  *y1 *y2 *y3 *y4 *y5 x1 x2 *x3 x4 x5
  +  *y1 *y2 *y3 *y4 y5 *x1 x2 x3 *x4 x5
  +  *y1 *y2 *y3 y4 *y5 x1 x2 x3 *x4 *x5
  +  *y1 *y2 y3 *y4 *y5 x1 x2 *x3 x4 x5
  +  *y1 y2 *y3 y4 y5 *x1 x2 *x3 *x4 x5
  +  *y1 y2 y3 *y4 *y5 *x1 x2 x3 *x4 x5
  +  y1 *y2 y3 *y4 *y5 *x1 x2 *x3 x4 *x5
  +  y1 *y2 y3 y4 y5 *x1 *x2 x3 *x4 x5
  +  y1 y2 *y3 y4 y5 *x1 x2 *x3 *x4 *x5
  +  y1 y2 y3 y4 *y5 x1 *x2 *x3 *x4 *x5

ABSTRACTION
  +  *x1 *x2 x3 *x4 x5
  +  *x1 x2 *x3 *x4
  +  *x1 x2 *x3 x4 *x5
  +  x1 *x2 *x3 *x4 *x5
  +  x1 x2 x3 *x4 *x5

ORIGINAL (MIXED ORDER)
  +  *x1 *x2 y1 *y2 y3 y4 y5 x3 *x4 x5
  +  *x1 x2 *y1 *y2 *y3 *y4 y5 x3 *x4 x5
  +  *x1 x2 *y1 y2 *y3 y4 y5 *x3 *x4 x5
  +  *x1 x2 *y1 y2 y3 *y4 *y5 x3 *x4 x5
  +  *x1 x2 y1 *y2 y3 *y4 *y5 *x3 x4 *x5
  +  *x1 x2 y1 y2 *y3 y4 y5 *x3 *x4 *x5
  +  x1 *x2 y1 y2 y3 y4 *y5 *x3 *x4 *x5
  +  x1 x2 *y1 *y2 *y3 *y4 *y5 *x3 x4 x5
  +  x1 x2 *y1 *y2 *y3 y4 *y5 x3 *x4 *x5
  +  x1 x2 *y1 *y2 y3 *y4 *y5 *x3 x4 x5

ABSTRACTION
  +  *x1 *x2 x3 *x4 x5
  +  *x1 x2 *x3 *x4
  +  *x1 x2 *x3 x4 *x5
  +  x1 *x2 *x3 *x4 *x5
  +  x1 x2 x3 *x4 *x5

score 2 · Accepted Answer

x1 と x2 が BDD の最上位になるように変数が並べられている場合、単純で効率的な解決策が存在します。

2 番目の例として BDD を考えてみましょう。

最初の 2 つのレイヤーを (幅優先の順序で) トラバースして、4 つのサブ BDD を取得できます。の可能な組み合わせごとに 1 つx1,x2。これらのサブ BDD の 3 つはルートでy1あり、4 番目は空です (定数 False)。

これで、各サブ BDD の要素数を数えることができます (Knuth のVolume 4 Fascicle 1、Bitwise Tricks & Techniques; Binary Decision Diagramsの Algorithm C )。

サブ BDD の要素数が 1 より大きい場合はドロップし (親ノードから直接へのショートカットFalse)、それ以外の場合はそのままにします。

要素をカウントしながら部分的な結果を記憶することにより、このアルゴリズムをシングルパスで実行することができます。

score 1 · Accepted Answer

1 つのアプローチには、一意性の定義を直接翻訳することが含まれます。

R(x,y) and forall z . ~R(x,z) or y = z

実装は次のようになります。

def inspect(function, name, nvars):
    sys.stdout.write(name) # avoid print's trailing space or newline
    function.summary(nvars) # minterm count needs number of variables
    function.printCover()

import sys
from cudd import Cudd
m = Cudd()

nx = 2
ny = 3
x = [m.bddVar() for i in range(nx)]
y = [m.bddVar() for i in range(ny)]

R = (~x[0] & x[1] & (~y[0] & y[1] | y[1] & y[2]) |
     x[0] & ~x[1] & (y[0] ^ y[1]) & y[2] |
     ~x[0] & ~x[1] & y[0] & ~y[1] & ~y[2])

# This approach is independent of variable order.  We are free to enable
# reordering or call it explicitly.
m.reduceHeap()

inspect(R, 'R', nx+ny)

# Create auxiliary variables and selector function.
z = [m.bddVar() for i in range(ny)]
zcube = reduce(lambda a, b: a & b, z)
P = ~m.xeqy(y,z)

# A pair is in L iff:
#   - it is in R
#   - there is no other pair in R with the same x and different y
L = R & ~(R.swapVariables(y,z).andAbstract(P,zcube))

inspect(L, 'L', nx+ny)

そのコードを実行した結果:

R: 10 nodes 1 leaves 6 minterms
01-11 1
10101 1
10011 1
00100 1
0101- 1

L: 6 nodes 1 leaves 1 minterms
00100--- 1

最初の 2 つの変数は、ペアの最初の要素をエンコードします。次の 3 つの変数は、ペアの 2 番目の要素をエンコードします。最後の 3 つの変数は補助変数です。

このコードは、上記の式に DeMorgan を適用してを利用しandAbstractます。

algorithm - BDD で表される関係における一意のタプルの拡張検索

3 に答える 3

Related

Reference