問題タブ [binary-decision-diagram]

2つのゼロ抑制二分決定図の結合を計算するアルゴリズムは何ですか？

私は今何時間もそれを探しました、私はそれを見つけることができません。結果の定義はありますが、私が知る限り、それはKnuthの本にもありません。

特定の実装を通り抜ける必要はありません。実装の詳細は非常に気が散ります。

ZDDの結合fとgは{ a ∪ b | a ∈ f and b ∈ g }

縮小順序二分決定図(ROBDD) (入力がセット内にある場合に true と評価される関数として解釈される)として表される整数のセットがあり、これを Domain と呼び、整数関数 (これを呼び出す) F) ROBDD の配列として表される (結果のビットごとに 1 つのエントリ)。

ここで、F のドメインの画像を計算したいと思います。ドメインからすべてのアイテムを列挙し、F を適用し、結果を画像に挿入することで簡単に実行できるため、間違いなく可能です。しかし、これは指数関数的な複雑さ (ドメインのサイズに線形) を持つ恐ろしいアルゴリズムであり、私の直感では、より高速になる可能性があることがわかります。私は次の方向を検討してきました：

1. F のすべてのビットに Restrict(Domain) を適用する
2. 魔法をかける

しかし、2番目のステップは難しいことがわかりました。最初のステップの結果には、必要な情報が含まれています (少なくとも、90% の確信があります) が、正しい形式ではありません。それを「ROBDDとしてエンコードされたセット」に変換する効率的なアルゴリズムはありますか? 他のアプローチが必要ですか？

CUDD (C インターフェイス) の BDD での操作に行き詰まっています。イメージの計算 (BDD の状態から別の状態へ) を行うときにいくつかの変数を削除できるかどうか、および結果の BDD (最終 BDD) を移動する方法がわかりません。 ) すべての変数を取得するには、CUDD でそれができるかどうか誰か教えてください。乾杯

CUDD のマネージャーから変数を安全に削除できることを教えてください。v1 = Cudd_bddNewVar(manager)例: ;で 2 つの変数を登録します。とv2 = Cudd_bddNewVar(manager)。v2マネージャーから削除できますか?

Java（またはJavaバインディングを提供するもの）でのBDD（二分決定図）の実装に関する提案はありますか？このページをオンラインで見つけました：http：//www.mancoosi.org/~abate/avalaible-bdd-librariesですが、古くなっているかどうかはわかりません。それとも、Prologの実装を使用するだけで意味がありますか？

I'm trying to implement univariate polynomials using ZDDs, as suggested in a comment in an other question.

I've read the paper of S. Minato(you may download it here), but I don't understand how to implement the operations on these ZDDs.

この論文の考え方は、変数として使用して多項式を表すことができるということx^(2^i)です。たとえば、 のx^5 + x^3 + xように書き換えることができます。変数x^4x^1 + x^2x^1 + x^1ごとにノードを作成x^(2^i)し、乗算された "1 エッジ" 変数と加算された "0 エッジ" 変数を接続すると、その多項式を表すグラフを簡単に取得できます。 . ZDD は、グラフに何らかの条件を適用するこの種のグラフです (詳細については、湊の記事と BDD に関するウィキペディアのページを参照してください)。

係数は、2 のべき乗の合計を使用して同様に表すことができます (たとえば、5 = 2^2 + 2^0すべて2^iが変数であり、ノードは同じ方法で 1 エッジと 0 エッジで接続されます)。

さて、私の問題は、2 つの ZDD を加算するアルゴリズムです。アルゴリズムは非常に単純に見えます。

F と G (ZDDs) に共通する組み合わせがない場合、それらをマージするだけで加算 (F + G) を完了できます。それらにいくつかの一般的な組み合わせが含まれている場合、次の式を計算します: (F + G) = S + (Cx2)、ここで C = F ∩ G、S = (FUG) \ C . このプロセスを繰り返すことで、最終的に共通の組み合わせがなくなり、手順が完了します。

問題は、「C」と「S」を効率的に見つけるにはどうすればよいかということです。

著者は乗算のコードを提供していますが、以前のアルゴリズムを実装すれば、コードは実際には簡単です。また、これらのアルゴリズムは提供されていないため、乗算も「役に立たない」ものです。

また、「マージ」ZDD の概念は十分に説明されていませんが、変数の順序が一貫していなければならないという事実を考慮すると、グラフをマージする方法は 1 つしかなく、この順序を維持するためのルールはおそらく単純です。十分です（まだ形式化していませんが、これらが何であるかについては大まかな考えがあります）。

リレーション内のタプルのセットを表すためにBDDを使用するとします。簡単にするために、0または1の値を持つタプルを検討してください。例：R = {<0,0,1>、<1,0,1>、<0,0,0>}は、x、y、zなどの3つの変数を持つBDDの三項関係を表します（1つは各タプルの要素）。私が欲しいのは、Rのようなbddを与え、キューブCが、Cの変数が抽象化されたときに、一意のタプルを含むRのサブセットを返す操作を実装することです。

たとえば、Cに変数x（各タプルの最初の要素を表す）が含まれている場合、関数の結果は{<0,0,0>}である必要があります。xが抽象化されると、タプル<0,0,1>と<1,0,1>が「同じ」になることに注意してください。

ここで、R = {<0,0,1>、<1,0,1>、<0,0,0>、<1,0,0>}であり、xを再度抽象化するとします。この場合、xを抽象化した後、Rに一意のタプルがないため、結果として定数falseが期待されます。

どんな助けでも大歓迎です。

指定された真理値表 (何らかのテキスト形式) から縮小順序付き二分決定図 (ROBDD) を作成するソフトウェア パッケージ (ライブラリではなく、アプリケーションが望ましい) はありますか?

私はルールを平易な英語の文よりも形式的に表現しようと試みており、ルールを説明するために命題アプローチとある種の二分決定木を使用する方向性を期待していました。

指定されたゾーンの外側にあるオブジェクトが、redState考慮されるために特定の状態 (たとえば ) にある必要があるとしsafeます。平易な英文で表現。

オブジェクトが ZoneA の外にあり、RedState にある場合、それは Safe です。

ただし、場合によっては、オブジェクトがこの制限から除外されることがあります。

オブジェクトが ZoneA の外にあり、RedState になく、Exempt である場合、それは安全です。

オブジェクトが ZoneA の外にあり、RedState になく、Exempt でない場合、それは安全ではありません。

ゾーン A のオブジェクトが赤色の状態であるかどうかは重要ではありません。残りのルールは次のとおりです。

オブジェクトがゾーン A に含まれている場合、そのオブジェクトは安全です。

命題定式化を使用して、これらのルールは次のように表現できると考えました。

¬ InZoneA∧ RedState⇒Safe

¬ InZoneA∧ ¬ RedState∧ Exempt ⇒Safe

¬ InZoneA∧ ¬ RedState∧ Exempt ⇒ ¬Safe

インゾーンA ⇒Safe

私はシステム仕様のアプローチ (Z など) について調べてきましたが、より大きなシステム内でルールが確実に機能するようにすることよりも、ルールの簡潔な概念を伝えることに関心があります。そこで、二分決定木（ダイアグラム）の一種で表現しようと考えました。この件に関するいくつかのメモを読みましたが、それらの使用が最善のアプローチなのか、それとも私がそれらを解体しているのかについて少し確信が持てません. これらのルールについて私がたどり着いた表現を図に示します。実線はTrueを、破線は を示していますFalse。

この表現が正しいかどうか、または私のアプローチ/考え方に欠陥があるかどうかについて、ご意見をいただければ幸いです。どうもありがとう！