真理値表からの BDD の構築

クヌース先生のアルゴリズム本の4巻を読んでいる。BDD の話が載っているので簡単に Java で実装していく。
まず、BDD のノードのクラスは、

public BddNode Zero = new BddNode(0, null, null); // 終点となる 0ノードと
public BddNode One = new BddNode(0, null, null); // 1ノード

public class BddNode{
		private int level = 0; // 変数レベル
		private BddNode left, right; // 0-枝、1-枝
		
		public BddNode(int num,BddNode lhs, BddNode rhs) {
			level = num;
			left = lhs;
			right = rhs;
		}
		
		public boolean isZeroNode() {
			return this == Zero;
		}
		
		public boolean isOneNode() {
			return this == One;
		}
		
		public BddNode getLeftNode() {
			return right;
		}
		
		public BddNode getRightNode() {
			return left;
		}
		
		public int getLevel() {
			return level;
		}
		
		public String getString() {
			if(this == Zero)
				return new String("0");
			else if(this == One)
				return new String("1");
			return new String("(" + Integer.toString(level) +
					"| " + left.getString() + ", " + right.getString() + ")");
		}
		
		public boolean equals(BddNode node) {
			if(level == node.level &&
					left == node.left &&
					right == node.right )
				return true;
			return false;
		}
	}

真理値表は、00010111 のような形をしている。この場合は、変数がx1,x2,x3 あり、先頭から (x1, x2, x3) = (0, 0, 0) の時の真理値、(0, 0, 1) の時の真理値、(0, 1, 0) の時の真理値 ...、(1, 1, 1)の時の真理値となる。つまり、x1, x2, x3 のすべての真理値の組み合わせ2^3 = 8 通りに対応した2進列になっている。

真理値表 00010111 を半分に分割すると、 0001, 0111 となり、前半が x1 が０の時、後半が x1 が１の時の真理値表になる。そして、半分に分割していった真理値表が BDD のノードに対応している。ということで、真理値表を再帰で半分に分割しながら、BDD を組み立てるアルゴリズムがこちら。

Vector< Vector<BddNode> > nodeStore = new Vector<>(); // 作成済みの BDD のノードを変数レベルごとに保存
	
public void init() {
		nodeStore.add(new Vector<>());
}
	
// 真理値表の長さから現在の変数レベルを求める	
public int getVariableLevel(int boolTableLength) {
	int cnt = 0;
	while(boolTableLength > 0) {
		++cnt;
		boolTableLength /= 2;
	}
	return cnt-1;
}

// 作成済みのノードから同じものを検索する
public BddNode search(BddNode node) {
	if(nodeStore.size() <= node.getLevel())
		return null;
	Vector<BddNode> sameLevelNodes = nodeStore.elementAt(node.level);
	for(int i = 0; i < sameLevelNodes.size(); ++i) {
		if(node.equals(sameLevelNodes.elementAt(i)))
				return sameLevelNodes.elementAt(i);
	}
	return null; // なかったら null を返す
}

// 作成した重複のないノードを保存する
public void register(BddNode node) {
	while(node.getLevel() >= nodeStore.size()) {
		nodeStore.add(new Vector<>());
	}
	nodeStore.elementAt(node.getLevel()).addElement(node);
}


// 再帰して BDD の下のノードから作成し、統合していく
public BddNode createBddFromBooleanTable(int front, int back, String boolTable) {
	// 真理値表の長さが 1 のとき、その真理値に対応した 0ノード、1ノードを返す
	if(back-front == 1) { 
		if(boolTable.charAt(front) =='0')
			return Zero;
		else if(boolTable.charAt(front)=='1')
			return One;	
	}
	
        // 現在の変数レベルが０の時、真理値表の左半分に対応するので、
	int mid = (back - front) / 2;
        // 0枝の先に左半分のノード
	BddNode retBddLeft = createBddFromBooleanTable(front, front + mid, boolTable);
        // 現在の変数レベルが１の時、右半分に対応し1枝の先のノード
	BddNode retBddRight = createBddFromBooleanTable(front + mid, back, boolTable);
	// 両方とも0ノード、もしくは、1ノードのとき対応する０ノード、1ノードを返す
	if(retBddLeft.isZeroNode() && retBddRight.isZeroNode())
		return Zero;
	if(retBddLeft.isOneNode() && retBddRight.isOneNode())
		return One;
		
	// 現在のノードを作り、
	BddNode currentNode = new BddNode(getVariableLevel(back-front),
			retBddLeft, retBddRight);
        // 重複がないか検索する
	BddNode sameNode = search(currentNode);
	if(sameNode == null) { // 重複がないなら登録し、そのノードを返す
		register(currentNode);
		return currentNode;
	}
        // 同じのがあったら、それを返す
	return sameNode;
}

もっと簡単にできると思ったら、ノードの重複を調べる処理で以外に長くなった。しかし、ただ単純にボトムアップに組み立てるなら、別に再帰する必要はない。再帰関数が書きたくなったから、上のように書いたけど。普通にボトムアップに組み立てるのが以下のコード。

public BddNode searchIn(BddNode node, BddNode[] nodes, int lastIndex) {
	for(int i=0; i < lastIndex; ++i) {
		if(node.equals(nodes[i]))
			return nodes[i];
	}
	return null;
}
	
public BddNode createBddBottomUp(String boolTable) {
        // 初めに、真理値表の0,1に対応したノードを prevNode に入れておく。
        // これをprevNode[i], prevNode[i+1] を組み合わせて次のレベルのノードをボトムアップに作っていく
	BddNode[] prevNodes = new BddNode[boolTable.length()];
	for(int i = 0; i < boolTable.length(); ++i) {
		if(boolTable.charAt(i) == '0') {
			prevNodes[i] = Zero;
		}else
			prevNodes[i] = One;
	}
		
	int varLevel = 0;
		
	for(int i=2; i <= boolTable.length(); i *= 2) { // 2つずつ組み合わせるので半分に減っていく
		BddNode[] nextNodes = new BddNode[boolTable.length() / i]; // 次のノードは現在のノードの半分
		++varLevel;
			
		for(int j=0; j < prevNodes.length; j += 2) {
                        // 二つのノードを組み合わせて次のノードを作る 
			if(prevNodes[j] == Zero && prevNodes[j + 1] == Zero)
				nextNodes[j / 2] = Zero;
			else if(prevNodes[j] == One && prevNodes[j + 1] == One)
				nextNodes[j / 2] = One;
			else {
				nextNodes[j / 2] 
						= new BddNode(varLevel,
								prevNodes[j], prevNodes[j + 1]);
                                // 重複を調べる
				BddNode retNode = searchIn(nextNodes[j / 2], nextNodes, j / 2);
　　　　　　　　　// 重複があったら、そのノードをセットする
				nextNodes[j / 2] = (retNode != null ? retNode : nextNodes[j / 2]);
			}
		}
		prevNodes = nextNodes;
	}
	return prevNodes[prevNodes.length-1]; // 最後のノードが全体の BDD 
}

こっちの方がシンプルになる。BDD を構成する関数を描いたが、何がBDDでできるかが問題