限量子付ブール式の充足可能性判定を用いた論理式の最小因数分解手法

• Item type: SIG Technical Reports(1)
• 公開日: 2005-11-30
• タイトル: 限量子付ブール式の充足可能性判定を用いた論理式の最小因数分解手法
• タイトル / 言語: en
• タイトル: Exact Minimum Logic Factoring via Quantified Boolean Satisfiability
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京大学大学院工学系研究科電子工学専攻
• 著者所属: 東京大学大規模集積システム設計教育研究センター（VDEC）
• 著者所属: 東京大学大規模集積システム設計教育研究センター（VDEC）
• 著者所属(英): en
• 著者所属(英): Department of Electronic Engineering University of Tokyo
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center(VDEC) University of Tokyo
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center(VDEC) University of Tokyo
• 著者名: 書田, 浩章; 二瀧田, 誠; 浅田, 邦博
• 著者名(英): Hiroaki, YOSHIDA; Makoto, IKWDA; Kunihiro, ASADA
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本稿では不完全定義論理関数の最小因数分解形表現を発見する厳密手法を提案する．提案手法では因数分解問題を限量子付プール式として表現し，この解を汎用の充足可能性判定手法によって求める．また我々はX-B木と呼ばれる新しいグラフ構造を提案する．X-B木は暗黙的にすべての可能な二分木構造を網羅しており，これを用いることにより因数分解問題を効率的に表現することが可能となっている．最後に例題を用いた計算機実験の結果を示し，本手法の妥当性を示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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 l2 literals.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 情報処理学会研究報告システムLSI設計技術（SLDM）; 巻 2005, 号 121(2005-SLDM-122), p. 173-178, 発行日 2005-11-30
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会