クヌース先生のアルゴリズム本の4巻を読んでいる。BDD の話が載っているので簡単に Java で実装していく。
まず、BDD のノードのクラスは、
public BddNode Zero = new BddNode(0, null, null);
public BddNode One = new BddNode(0, null, null);
public class BddNode{
private int level = 0;
private BddNode left, right;
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<>();
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;
}
public void register(BddNode node) {
while(node.getLevel() >= nodeStore.size()) {
nodeStore.add(new Vector<>());
}
nodeStore.elementAt(node.getLevel()).addElement(node);
}
public BddNode createBddFromBooleanTable(int front, int back, String boolTable) {
if(back-front == 1) {
if(boolTable.charAt(front) =='0')
return Zero;
else if(boolTable.charAt(front)=='1')
return One;
}
int mid = (back - front) / 2;
BddNode retBddLeft = createBddFromBooleanTable(front, front + mid, boolTable);
BddNode retBddRight = createBddFromBooleanTable(front + mid, back, boolTable);
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) {
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) {
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でできるかが問題
