| 講演名 | 2005-12-02 限量子付ブール式の充足可能性判定を用いた論理式の最小因数分解手法(VLSIの設計/検証/テスト及び一般(デザインガイア)) 吉田 浩章, 池田 誠, 浅田 邦博, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では不完全定義論理関数の最小因数分解形表現を発見する厳密手法を提案する.提案手法では因数分解問題を限量子付ブール式として表現し, この解を汎用の充足可能性判定手法によって求める.また我々はX-B木と呼ばれる新しいグラフ構造を提案する.X-B木は暗黙的にすべての可能な二分木構造を網羅しており, これを用いることにより因数分解問題を効率的に表現することが可能となっている.最後に例題を用いた計算機実験の結果を示し, 本手法の妥当性を示す. |
| 抄録(英) | This paper presents an exact algorithm which finds the minimum factored form of an incompletely specified Boolean function. The problem is formulated as a Quantified Boolean Formula (QBF) and is solved by general-purpose QBF solver. We also propose a novel graph structure, called an X-B tree, which implicitly enumerates binary trees. Using this graph structure, the factoring problem is compactly transformed into a QBF and hence the size of solvable problems is extended. Experimental results show that the proposed algorithm successfully finds the exact minimum solutions to the problems with up to 12 literals. |
| キーワード(和) | 限量子付ブール式 / 充足可能性判定 / 因数分解 / 二分木 |
| キーワード(英) | Quantified Boolean formula / Boolean satisfiability / logic factoring / binary tree |
| 資料番号 | VLD2005-83,ICD2005-178,DC2005-60 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2005/11/25(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 限量子付ブール式の充足可能性判定を用いた論理式の最小因数分解手法(VLSIの設計/検証/テスト及び一般(デザインガイア)) |
| サブタイトル（和） | |
| タイトル（英） | Exact Minimum Logic Factoring via Quantified Boolean Satisfiability |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 限量子付ブール式 / Quantified Boolean formula |
| キーワード(2)（和/英） | 充足可能性判定 / Boolean satisfiability |
| キーワード(3)（和/英） | 因数分解 / logic factoring |
| キーワード(4)（和/英） | 二分木 / binary tree |
| 第 1 著者 氏名（和/英） | 吉田 浩章 / Hiroaki YOSHIDA |
| 第 1 著者 所属（和/英） | 東京大学大学院工学系研究科電子工学専攻 Department of Electronic Engineering, University of Tokyo |
| 第 2 著者 氏名（和/英） | 池田 誠 / Makoto IKEDA |
| 第 2 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター(VDEC) VLSI Design and Education Center(VDEC), University of Tokyo |
| 第 3 著者 氏名（和/英） | 浅田 邦博 / Kunihiro ASADA |
| 第 3 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター(VDEC) VLSI Design and Education Center(VDEC), University of Tokyo |
| 発表年月日 | 2005-12-02 |
| 資料番号 | VLD2005-83,ICD2005-178,DC2005-60 |
| 巻番号（vol） | vol.105 |
| 号番号（no） | 443 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |