おねえさんを組み合わせ爆発から救う:無駄を省いてBDDを作る

おねえさんを組み合わせ爆発から救うために、経路を二分決定木として表しました。
http://d.hatena.ne.jp/nowokay/20121016#1350351212


前回の二分決定木を見ると、「1:2」「1:3」を通るとした場合、あとはどのような選択をしても単純な経路にならず「F」にたどりつきます。同様に、両方通らない場合も「F」になります。
このように、それ以降はどのような選択をしても結果がひとつに決まるという場合、それ以降のツリーを省略すると、決定木がすっきりします。


また、それ以降の分岐が等しくなる場合をまとめることもできます。そうすると、単純な二分決定木ではとても画面におさまりきらなかった2x2マスの経路も表示できるようになります。

このような図はツリーではなくなっているので、二分決定図、BDD(Binary Decision Diagram)といいます。この図では、「T」「F」をそれぞれ表示していますが、実際にはひとつだけ表示します。
分岐のどちらを通っても結果が同じになる場合は、その分岐を省略することもできます。ただ、今回の経路問題では、ある辺を通っても通らなくても、他の経路が変わらないということがありえないので、そのような省略はあらわれません。


とりあえず、3x3マスの経路のBDDも、画面に収まるようになります。宇宙船っぽい。

多くの場合で、BDDは単純な二分決定木より節点や辺の数が大幅に削減できます。こうすることで、論理関数のすべての解をコンパクトに保持することができます。


おねえさんをロボットにさせた問題が、ちょっとだけ見えてきました。


BDDについては、The Art of Computer Proguramingの7.1.4で詳しく解説されています。


目次
『フカシギの数え方』 おねえさんといっしょにみんなも25万年数えよう
おねえさんを組み合わせ爆発から救う:格子グラフを生成する
おねえさんを組み合わせ爆発から救う:2分決定木を作る
おねえさんを組み合わせ爆発から救う:無駄を省いてBDDを作る
おねえさんを組み合わせ爆発から救う:ZDDがおねえさんを救う
おねえさんを組み合わせ爆発から救う:完結編おねえさんは星になった


ソースはこれで。動かすにはこれまでの2つのソースも必要です。

package simpath;

import java.awt.Graphics2D;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import kis.jgraphsample.CreateLattice.LatticeEdge;
import kis.jgraphsample.CreateLattice.LatticeNode;
import kis.jgraphsample.CreateTree.DiagramNode;
import kis.jgraphsample.CreateTree.EdgeNode;
import kis.jgraphsample.CreateTree.LeafNode;

public class CreateBdd {
    public static void main(String[] args){
        //格子グラフの生成
        ArrayList<LatticeEdge> edges = new ArrayList<>();
        Map<Integer, LatticeNode> nodeMap = new LinkedHashMap<>();
        CreateLattice.generateGraph(2, nodeMap, edges);

        String param = solveRoute(edges, nodeMap);
        
        //BDDの生成
        //param = "fftftffffftftffffftfttfftftffftt";
        List<List<DiagramNode>> layers = createBdd(edges, param);
        
        //表示
        CreateTree.paintDiagram(layers, 250, 250, 40, 50);
        //CreateTree.paintDiagram(layers, 590, 700, 40, 50);
        //CreateTree.paintDiagram(layers, 1750, 800, 35, 30);
    }
    /** BDDの生成 */
    static List<List<DiagramNode>> createBdd(ArrayList<LatticeEdge> edges, String param) {
        List<List<DiagramNode>> layers = new ArrayList<>();
        List<DiagramNode> layer = new ArrayList<>();
        layers.add(layer);
        Map<String, EdgeNode> edgeMap = new HashMap<>();
        ThroughNode tn = new ThroughNode();
        createBdd(layers, edges, edgeMap, 0, param, tn, false);
        return layers;
    }
    /** BDD各ノードの生成 */
    static void createBdd(List<List<DiagramNode>> layers,
            ArrayList<LatticeEdge> edges,
            Map<String, EdgeNode> edgeMap,
            int height, String param, EdgeNode en, boolean pre)
    {

        if(layers.size() <= height){
            layers.add(new ArrayList<DiagramNode>());
        }
        List<DiagramNode> layer = layers.get(height);
        
        LeafNode ln = null;
        if(param.indexOf("f") < 0){
            //tだけ
            ln = new LeafNode(true);
        }else if(param.indexOf("t") < 0){
            //fだけ
            ln = new LeafNode(false);
        }
        if(ln != null){
            //t・fが決まった
            if(pre){
                en.right = ln;
            }else{
                en.left = ln;
            }
            layer.add(ln);
            return;
        }

        String left = param.substring(0, param.length() / 2);
        String right = param.substring(param.length() / 2);
        if(left.equals(right)){
            //左右が同じ
            ThroughNode tn = new ThroughNode();
            if(pre){
                en.right = tn;
            }else{
                en.left = tn;
            }
            layer.add(tn);
            //くりかえす
            createBdd(layers, edges, edgeMap, height+1, left, tn, pre);
            return;
        }
        //分岐の生成
        EdgeNode nn = edgeMap.get(param);
        boolean gen = false;
        if(nn == null){
            //新しくでた組み合わせ
            gen = true;
            LatticeEdge le = edges.get(height);
            nn = new EdgeNode(le);
            layer.add(nn);
            edgeMap.put(param, nn);
        }
        if(pre){
            en.right = nn;
        }else{
            en.left = nn;
        }
        //くりかえす
        if(gen){
            createBdd(layers, edges, edgeMap, height+1, left, nn, false);
            createBdd(layers, edges, edgeMap, height+1, right, nn, true);
        }
    }

    static String solveRoute(ArrayList<LatticeEdge> edges, Map<Integer, LatticeNode> nodeMap) {
        //解答パターンの生成
        long count = 1L << edges.size();//パターン数
        StringBuilder result = new StringBuilder();
        int tcount = 0;
        LOOP: for(long i = 0; i < count; ++i){
            Map<Integer, List<LatticeEdge>> counter = new HashMap<>();
            long flag = count;
            for(CreateLattice.LatticeEdge edge : edges){
                flag >>= 1;
                if((flag & i) != 0){
                    if(!CreateTree.checkWrongRoute(counter, edge.from.num, edge, nodeMap.size())){
                        result.append("f");
                        continue LOOP;
                    }
                    if(!CreateTree.checkWrongRoute(counter, edge.to.num, edge, nodeMap.size())){
                        result.append("f");
                        continue LOOP;
                    }
                }
            }
            if(CreateTree.checkRoute(counter, nodeMap.size())){
                result.append("t");
                ++tcount;
            }else{
                result.append("f");
            }
        }
        System.out.println(tcount + "/" + result.length());
        return result.toString();
    }

    static class ThroughNode extends EdgeNode{

        public ThroughNode() {
            super(null);
        }

        @Override
        public void paint(Graphics2D g) {
        }
    }
}