WEKO3
-
RootNode
アイテム
論理関数のCNFからBDDの効率的な構築法
https://ipsj.ixsq.nii.ac.jp/records/95728
https://ipsj.ixsq.nii.ac.jp/records/95728e95a375d-e40e-442e-a754-f6083237b539
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-AL13145003.pdf (922.0 kB)
|
Copyright (c) 2013 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2013-10-30 | |||||||
| タイトル | ||||||||
| タイトル | 論理関数のCNFからBDDの効率的な構築法 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Efficient Construction of BDDs from CNFs | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 科学技術振興機構ERATO湊離散構造処理系プロジェクト | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| ERATO MINATO Discrete Structure Manipulation System Project, Japan Science and Technology Agency | ||||||||
| 著者名 |
戸田貴久
× 戸田貴久
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 論理関数の CNF が与えられるとき，その論理式を表す二分決定グラフ BDD を構築するための新しい手法を提案する．CNF は従来から用いられている論理関数の伝統的な表現法の一つである．BDD には論理関数を操作するための様々な演算が備わっているので，CNF よりも BDD を用いる方が適切な多くの問題がある．しかし，CNF から BDD の構築は自明な計算ではない．本稿では，まず CNF を表す中間表現を計算し，それから BDD に変換する二段階の BDD 構築法を提案する．さらに，提案法で中間表現として用いられるデータ構造は，BDD 構築だけでなく，有向グラフ上の列挙問題など様々な問題に対して有用であることも示す． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 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. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN1009593X | |||||||
| 書誌情報 |
研究報告アルゴリズム（AL） 巻 2013-AL-145, 号 3, p. 1-8, 発行日 2013-10-30 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
