論理関数のCNFからBDDの効率的な構築法 Efficient Construction of BDDs from CNFs

この論文にアクセスする

この論文をさがす

著者

    • 戸田貴久
    • 科学技術振興機構ERATO湊離散構造処理系プロジェクト ERATO MINATO Discrete Structure Manipulation System Project, Japan Science and Technology Agency

抄録

論理関数の 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.

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.

収録刊行物

  • 研究報告アルゴリズム(AL)

    研究報告アルゴリズム(AL) 2013-AL-145(3), 1-8, 2013-10-30

    一般社団法人情報処理学会

各種コード

  • NII論文ID(NAID)
    110009614883
  • NII書誌ID(NCID)
    AN1009593X
  • 本文言語コード
    JPN
  • 資料種別
    Technical Report
  • ISSN
    0913-5685
  • NDL 記事登録ID
    025085395
  • NDL 請求記号
    Z16-940
  • データ提供元
    NDL  NII-ELS  IPSJ 
ページトップへ