| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2026-03-04 10:00 扱いやすいブール論理式から二分決定グラフへの変換の計算複雑性 ジョバンニ ブッゼーガ（ピサ大）・○栗田和宏（岡山大）・脊戸和寿（北大）  COMP2025-21 |
|
| 抄録 | （和） | 本研究ではブール論理式が与えられたとき，その真理値表と等価な二分決定グラフ（Binary Decision Diagram, BDD）を計算する問題の計算複雑性について議論する． 二分決定グラフとは真理値表の有向非巡回グラフ表現であり，ある真理値表を表現する二分決定グラフは一般には複数存在する． ある真理値表を表す最小サイズの二分決定グラフは一意になることが知られているため，本研究では与えられたブール論理式を表す最小サイズの二分決定グラフを計算する問題を考える． この計算問題に対し計算複雑性を議論するとき，入力のブール論理式に対し，出力の二分決定グラフのサイズは指数的に大きくなることがありうるため，本研究ではこの問題に対する出力依存型の計算複雑性について議論する． また，ブール論理式が非充足の場合，二分決定グラフのサイズが入力サイズの線形で抑えられることが知られている．この事実から，ブール論理式の非充足判定問題が多項式時間で解けない場合， P ≠ NP の仮定のもとこの問題に対する出力多項式時間アルゴリズムは存在しない．そこで本研究では 2-SAT や Horn-SAT， Monotone-SAT のような，充足可能性問題が多項式時間で解けるブール論理式を対象に，ブール論理式の二分決定グラフへの変換問題の計算複雑性を議論する． |
| （英） | In this paper, we discuss the complexity of the problem of transforming a given Boolean formula $f$ into a binary decision diagram (BDD) that is equivalent to the Boolean function represented by $f$. A Binary Decision Diagram is a directed acyclic graph representation of a truth table, and in general, multiple BDDs may represent the equivalent Boolean function. It is known that the minimum-size BDD representing a given Boolean function is unique. Thus, we consider the problem of transforming a Boolean function $f$ into the minimum-size BDD that represents $f$. When analyzing the complexity of this problem, it is important to note that the size of the output BDD may be exponentially larger than the size of the input formula. Hence, we investigate the output-sensitive complexity of this problem. Moreover, it is known that if a Boolean formula is unsatisfiable, the size of its BDD can be bounded linearly in the input size. This implies that, unless unsatisfiability can be decided in polynomial time, no output-polynomial time algorithm for this problem exists under the assumption that $P neq NP$. For this reason, we focus on classes of Boolean formulas for which the satisfiability problem is solvable in polynomial time, such as 2-CNF, Horn-CNF, and XOR-CNF, and we discuss the complexity of transforming such Boolean formulas into BDDs. |
|
| キーワード | （和） | 二分決定図 / 計算困難性 / 出力依存型アルゴリズム / / / / / |
| （英） | Binary Decision Diagram / NP-hardness / Output Sensitive algorithm / / / / / | |
| 文献情報 | 信学技報, vol. 125, no. 390, COMP2025-21, pp. 1-4, 2026年3月. | |
| 資料番号 | COMP2025-21 | |
| 発行日 | 2026-02-25 (COMP) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | COMP2025-21 |
|
| 研究会情報 | |
| 研究会 | COMP |
| 開催期間 | 2026-03-04 - 2026-03-04 |
| 開催地（和） | 中央大学後楽園キャンパス 6号館4階6402 |
| 開催地（英） | Chuo University Korakuen Campus Building 6 4F Room 6402 |
| テーマ（和） | 理論計算機科学，一般 |
| テーマ（英） | Theoretical Computer Science, General |
| 講演論文情報の詳細 | |
| 申込み研究会 | COMP |
| 会議コード | 2026-03-COMP |
| 本文の言語 | 英語（日本語タイトルあり） |
| タイトル（和） | 扱いやすいブール論理式から二分決定グラフへの変換の計算複雑性 |
| サブタイトル（和） | |
| タイトル（英） | On the Complexity of Transformation from Tractable Boolean Formulas to Binary Decision Diagrams |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 二分決定図 / Binary Decision Diagram |
| キーワード(2)（和/英） | 計算困難性 / NP-hardness |
| キーワード(3)（和/英） | 出力依存型アルゴリズム / Output Sensitive algorithm |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | ジョバンニ ブッゼーガ / Giovanni Buzzega / ジョバンニ ブッゼーガ |
| 第1著者 所属（和/英） | ピサ大学 (略称： ピサ大) Pisa University (略称： PU) |
| 第2著者 氏名（和/英/ヨミ） | 栗田 和宏 / Kazuhiro Kurita / クリタ カズヒロ |
| 第2著者 所属（和/英） | 岡山大学 (略称： 岡山大) Okayama University (略称： OU) |
| 第3著者 氏名（和/英/ヨミ） | 脊戸 和寿 / Kazuhisa Seto / セト カズヒサ |
| 第3著者 所属（和/英） | 北海道大学 (略称： 北大) Hokkaido University (略称： HU) |
| 講演者 | 第2著者 |
| 発表日時 | 2026-03-04 10:00:00 |
| 発表時間 | 30分 |
| 申込先研究会 | COMP |
| 資料番号 | COMP2025-21 |
| 巻番号（vol） | vol.125 |
| 号番号（no） | no.390 |
| ページ範囲 | pp.1-4 |
| ページ数 | 4 |
| 発行日 | 2026-02-25 (COMP) |
[研究会発表申込システムのトップページに戻る]