4

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

4

4 に答える 4

6

これを試すこともできます: http://formal.cs.utah.edu:8080/pbl/BDD.php

これは、これまで使用した BDD に最適なツールです。

于 2013-06-10T14:48:39.107 に答える
1

BDD は、重複する部分真実表の検出に大きく依存しているため、メモリに制約のあるデータ構造です。目にするほとんどの BDD パッケージは、大規模な一般的な真理値表には正確に適合するものではなく、代わりに、非常にまばらな式や反復性の高い式用に最適化されています。

標準の BDD パッケージでは、変数を操作する式を使用します。したがって、真理値表を反復処理して、表内の 1 の積の式のようなものを作成する必要があります。その過程で、ほとんどのライブラリはメモリの制約に合わせて変数を動的に並べ替え、別の大幅な速度低下を引き起こします。約 24 個の変数の後、非常にまばらな真理値表であっても、これらのライブラリは最新のシステムでスラッシングし始めます。

変数の順序付けが既に暗黙的に定義されている真理値表が与えられた場合、最終的な BDD ノードのみを探している場合は、Unix テキスト処理ツールを使用するだけで、外部ライブラリと恐ろしいランタイムを使用して多くの複雑さをスキップできます。

BDD に関する優れたリソースである Knuth の TAOCP v4.1b は、BDD ノードとその「ビーズ」、つまり非正方形文字列である部分真実表の同等性を示しています。「zeads」と呼ばれる同様の構造を持つ、より単純なバージョンの ZDD について説明します。これは、完全にゼロではない正の部分の部分真理値表です。BDD に一般化するには、パイプラインの sed+grep を、ゼロ以外の正の部分の文字列を保持する代わりに、正方形の文字列をフィルタリングするプログラムに置き換えます。

真理値表のすべてのゼードを出力するには (ascii '1' と '0' の 1 行のファイルとして与えられ、末尾に改行があります)、変数の数とファイル名を設定した後、次のコマンドを実行します。

MAX=8; FILENAME="8_vars_truthtable.txt"; for (( ITER=0; ITER<=${MAX}; ITER++ )) ; do INTERVAL=$((2 ** ${ITER})); fold -w ${INTERVAL} ${FILENAME} | sed -n '1~2!p' | grep -v "^0*$" | sort -u ; done

これには、BDD パッケージよりも多くの利点があります。

  • 余分な依存関係が本質的にない単純なもの。
  • 外部ソートは、インメモリ ハッシュ テーブルとは異なり、スラッシングがないことを意味します。
  • for ループで fork するときのライン バッファリングとディスク キャッシングを理解していれば、簡単に並列化およびスケーラブルにできます。
  • 中間ファイルに書き込む場合、ソートも並列化されます。

BDD ライブラリを使用して現実的に考え出すことは不可能な最大 32 個の変数までの真理値表に定期的に使用しています。メモリ システムにはまったく負担をかけず、数 MB しか使用しません。しかし、利用可能な RAM が大量にある場合、Linux のような適切な OS は、ディスクをキャッシュしてさらに高速化するために喜んですべてを使用します。

于 2015-02-11T13:42:45.553 に答える
1

任意の BDD ライブラリを使用すると、必要なことを行うことができます。もちろん、自分でコードを書かなければなりません。

軽量のツールを探している場合、関数の BDD を簡単に調べるために、次のようなアプレットをよく使用します。

http://tams-www.informatik.uni-hamburg.de/applets/java-bdd/

于 2013-03-25T13:27:06.710 に答える