@techreport{oai:ipsj.ixsq.nii.ac.jp:00095728,
 author = {戸田貴久},
 issue = {3},
 month = {Oct},
 note = {論理関数の CNF が与えられるとき，その論理式を表す二分決定グラフ BDD を構築するための新しい手法を提案する．CNF は従来から用いられている論理関数の伝統的な表現法の一つである．BDD には論理関数を操作するための様々な演算が備わっているので，CNF よりも BDD を用いる方が適切な多くの問題がある．しかし，CNF から BDD の構築は自明な計算ではない．本稿では，まず CNF を表す中間表現を計算し，それから BDD に変換する二段階の BDD 構築法を提案する．さらに，提案法で中間表現として用いられるデータ構造は，BDD 構築だけでなく，有向グラフ上の列挙問題など様々な問題に対して有用であることも示す．, We propose an algorithm to construct the binary decision diagram (BDD) for a CNF formula of a Boolen function. A CNF formula is a usual representation of Boolean functions and has been used for a long time. On the other hand, various operations to manipulate Boolean functions are available in a BDD, and thus there are many problems where using BDDs are more efficient, however converting CNFs to BDDs is not a trivial task. In this paper, we propose a construction algorithm through two stages: we first compute an intermediate representation of a CNF formula, and then construct the corresponding BDD. We furthermore show that the data structure used as an intermediate representation is useful not only in BDD construction, but also in various problems such as enumeration problems on directed graphs.},
 title = {論理関数のCNFからBDDの効率的な構築法},
 year = {2013}
}