問題タブ [binary-decision-diagram]

次の定義を前提としています。

ブール式からROBDDを構築したい。これまでのところ、非冗長性または共有性を満たさない BDD を構築できました。

これはまだ進行中の作業であるため、ネーミングとスタイルは最適ではない可能性があります。

ノードは、一意の ID によって内部的に表されます。2 から始まります。左側のサブツリーのルート ノードには2nというラベルが付けられ、右側のサブツリーのルート ノードには2n + 1というラベルが付けられます。

この関数は、ブール式と、式に現れる変数のインデックスのリストを入力として受け取ります。

たとえば、次の式の場合:

コールbuildBDD bexp [2,3,7]が返ってきます

冗長性のないプロパティを考慮して、次の変更を加えました(これは完全にはテストされていませんが、機能しているようです)。

(上記の不自然な表現をお許しください)

ただし、特に共有ノードがグラフのどこかにある可能性があり、現在のツリーを保存していないため、共有プロパティにアプローチする方法がわかりません。一意のノード ID の式は、必要に応じて変更できます。

注: これは練習用であるため、関連する型とスタイルは最適ではない可能性があります。また、それらを変更することも想定されていません（機能を自由に変更できます）。