論理関数のCNFからBDDの効率的な構築法

摘要

論理関数のCNFが与えられるとき，その論理式を表す二分決定グラフBDDを構築するための新しい手法を提案する．CNFは従来から用いられている論理関数の伝統的な表現法の一つである．BDDには論理関数を操作するための様々な演算が備わっているので，CNFよりもBDDを用いる方が適切な多くの問題がある．しかし，CNFからBDDの構築は自明な計算ではない．本稿では，まずCNFを表す中間表現を計算し，それからBDDに変換する二段階のBDD構築法を提案する．さらに，提案法で中間表現として用いられるデータ構造は，BDD構築だけでなく，有向グラフ上の列挙問題など様々な問題に対して有用であることも示す．