CUDDの簡単な利用例: BDD構造の幅優先探索

TL; DR

• ランダムな論理関数を作成できるようになった
• BDD/ZDD/ADDのノードを表しているC言語側の構造体__DdNode(のポインタ)__を利用して、BDD構造を走査したい
• とりあえずqueueとstackを利用すれば幅優先・深さ優先探索ができる
• 優先探索からやってみる。

前提

• 実装済みのランダムな論理関数がBDDで返ってくる関数を__random_function__という名前で再利用
• DdNode*からBDDを作る場合は以下の形で可能（効率が良い/悪いまでは気にしない）

Cudd mgr;
DdNode* n = (何らかの内部構造へのポインタ)
BDD b = BDD(mgr, n);

• あるノードから0枝（点線）と1枝（実践）を辿った先のノードはそれぞれC言語側の関数__Cudd_E__と__Cudd_T__で取得できる

• あるBDDの節点bについて、その深さは関数__NodeReadIndex__で、子供に存在する節点数を__nodeCount__で取得できる

幅優先探索の実装

• 前提とqueueを利用して実装する

#include <iostream>
#include <random>
#include <vector>
#include <queue>
#include <stack>
#include "cuddObj.hh"
#include "myutil.hpp" // random_functionが入っている

using namespace std;

int main() {
  Cudd mgr;
  const int N = 4;
  vector<int> pos;
  BDD f = random_function(N, &pos, mgr);

  // dot dump
  const vector<ADD> vec = {f.Add()};
  const char* iname[4] = {"x1", "x2", "x3", "x4"};
  const char* oname[1] = {"F"};
  auto fp = fopen("dot/random.dot", "w");
  mgr.DumpDot(vec, iname, oname, fp);

  // BFS
  queue<DdNode*> q;
  q.push(f.getNode());
  while (!q.empty()) {
    DdNode* n = q.front(); q.pop();
    BDD b = BDD(mgr, n);
    std::string name = b.IsZero() ? "F" : (b.IsOne() ? "T" : iname[b.NodeReadIndex()]);
    cout << name << ":" << b.nodeCount() << "," << b.NodeReadIndex() << endl;

    // put left & right child only when n is an nternal nodes
    if (!b.IsZero() && !b.IsOne()) {
      DdNode* l = Cudd_E(n);
      DdNode* r = Cudd_T(n);
      q.push(l);
      q.push(r);
    }
  }
  return 0;
}

ランダム関数の例

出力の例

• おそらく合っている気持ちになる

x1:6,0             # 0x3a:root(x1)は自分以下に節点を6つ持つ
x2:4,1             # 0x3aの0枝側: x2は自分以下に節点を4つ持つ（0x36)
x2:3,1             # 0x3aの1枝側: x2は自分以下に節点を3つ持つ（0x39)
x3:3,2             # 0x36の0枝側： x3は自分以下に節点を3つ持つ（0x35)
T:1,2147483647     # 0x36の1枝側: T(=1)
x4:2,3             # 0x39の0枝側: x4は自分以下に節点を2つ持つ（0x31)
T:1,2147483647     # 0x39の1枝側: T(=1)
x4:2,3             # 0x35の0枝側: x4(0x31)
F:1,2147483647     # 0x35の1枝側: F(=0)
F:1,2147483647     # 0x31の0枝側: F(=0)
T:1,2147483647     # 0x31の1枝側: T(=1)