問題タブ [binary-decision-diagram]

Javaで実装しています。

現時点では、関係をデータ構造に格納するために BDD (Binary Decision Diagramms) を使用しようとしています。

たとえば、R={(3,2),(2,0)} と対応する BDD:

このため、BDD 機能を備えたライブラリを探していました。

JavaBDD と JDD の 2 つの可能性が見つかりました。

しかし、どちらの場合も、単純な整数を BDD にエンコードする方法がわかりません。なぜなら、整数の値をいつ、どのように与えるのでしょうか? または、二分決定グラフが整数で表される場合、それはどういう意味ですか?

どちらの場合も、次のような方法があります。

また

私の例のような BDD を簡単に作成するにはどうすればよいですか?

どうもありがとうございました！！

BDD 操作を行うために CUDD パッケージを使用しています。特定の変数順序を渡して、BDD の構築中にこの順序を使用するようにプログラムに指示する方法を誰かが知っているかどうか疑問に思っていました。変数の数が比較的少ないブール関数を使用しています。

実際、プログラムに特定の入力変数を渡して BDD をルートする方法があったとしても、それは私の目的にも役立ちます。誰かがこれを行う方法を知っていれば、本当に助けていただければ幸いです。ドキュメントを調べましたが、この趣旨のものが見つかりませんでした。多分私は何かを逃した。

{<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 の論理積、論理和、補数の操作を表す。

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

1. 私のアプローチの AC 実装、参照実装4と呼ばせてください。
2. 受け入れられた回答3でユーザー meolic によって提案された実装。
3. 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に関してすべての論理演算を実装した後、次の結果が得られました。

1. uniqueAbstractRecRef (21831 ミリ秒) 一意の抽象化統計: 呼び出しの総数: 1723239 最適化された呼び出し: 0 存在する抽象呼び出しの総数: 30955618 存在する抽象への一意の抽象呼び出し: 2385915 ite 呼び出しの総数: 3574555

2. uniqueAbstractSERec (56761 ミリ秒) 一意の抽象化統計: 呼び出しの総数: 193627 最適化された呼び出し: 60632 存在する抽象呼び出しの総数: 16475806

3. uniqueAbstractRec (20587 ミリ秒) 一意の抽象化統計: 呼び出しの総数: 270205 最適化された呼び出し: 78486 存在する抽象呼び出しの総数: 13186348

Reduced Ordered Binary Decision Diagram (ROBDD) で 8 クイーン パズル問題を解く方法がわかりません。私はそれをグーグルで検索しましたが、問題の適切な説明を見つけることができません。したがって、ここでの問題 - これまでのところ、n*n の入力変数または ROBDD の状態が存在することがわかりました。では、8 クイーン パズルを解く ROBDD を実際に作成するにはどうすればよいでしょうか。

1. ROBDD はどのようにこの問題の解決策を見つけることができますか?
2. 上記の問題のグラフ表現がわかりません
3. 最小数のノードを実際にどのように生成しますか?
4. 入力変数の順序はどうですか?
5. どのように削減されますか？

説明は、問題をよりよく理解するのに役立ちます。

与えられた二分決定図を真理値表に変換するにはどうすればよいですか? そのための正確なアルゴリズムは何ですか? 私はこれを長い間試してきました。以下は、従うことができる例です。

出典：ウィキペディア。

(点線のエッジは 0、実線のエッジは 1 を表します。)

固定長ビット配列と比較して、16 ビットの符号付き整数変数を間隔 (-32768..32767) として表すと、パフォーマンスが大幅に低下するのはなぜですか?

前処理された NuSMV/NuXMV モデルを調べると、間隔タイプが列挙型に変換されていることがわかります。

ただし、BDD の統計には、関連する情報は表示されません。

y (バイナリ クラス) を予測するために、いくつかの名前とその他の機能を使用しています。名前の特徴は、名前の部分文字列です。Python Scikit-learn を使用しています。

X の一部を次に示します。

次に、dictvectorization を使用して X をベクトル化し、これに...

問題は、新しい X が何を表しているのか完全に見失っていることです。また、決定木グラフを作成する必要があるため、解釈できない結果しか得られません。

私のpythonコード：