BDD/ZDDを用いたペントミノパズルの解の列挙  [in Japanese] Enumerating Solutions of the Pentomino Puzzle Using BDDs/ZDDs  [in Japanese]

二分決定グラフ(BDD)は,論理関数のグラフ表現であり,大規模な論理関数データでも比較的コンパクトなデータ構造として表現できる.さらに,BDDの特殊な型であるゼロサプレス型BDD(ZDD)は組合せ集合データの表現・処理に適しており,情報科学における様々な問題に応用できる.その一つの例が制約充足問題である.制約充足問題を解くために多くのアルゴリズムが考案されているが,その一方で,解集合の解析や新たな制約を加えて別の制約充足問題を解くということは,また別の問題として残っている.そこで,BDDまたはZDDで解全体を同時に表現することで,それらを効率よく行う方法を述べる.本稿では,古くから親しまれてきたペントミノパズルを取り上げ,これを制約充足問題として定式化した上でBDDとZDDに基づいた解法を示す.

Binary Decision Diagram (BDD) is a graph-based representation of Boolean function. BDDs can compactly represent and efficiently manipulate large-scale Boolean function data. Zero-suppressed BDD (ZDD) is a special type of BDD, which is suitable for representing and processing combinatorial set data. We can apply ZDDs for many kind of combinatorial problems in computer science. Constraint Satisfaction Problems (CSPs) are one of the typical examples where ZDDs are effective. Many algorithms have been developed for solving CSPs, but it is a different matter how to analyzing solutions and to extend the problem with additional constraints. BDDs/ZDDs can effectively be used for such tasks. In this paper, we pick up the Pentomino puzzle and present a good way of applying the BDD/ZDD-based method.