| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2008-12-19 10:00 基本対称関数を付加したCNF論理式の充足可能性判定 ○馬野洋平・酒井正彦・西田直樹・坂部俊樹・草刈圭一朗（名大）  SS2008-44 |
|
| 抄録 | （和） | 近年，高速な充足可能性判定ツール（SATソルバ）の開発が進んでいる． これらのツールでは，変数値を次々に推論するBCPという演算がSATソルバの実行時間の大半を占めていることが多く，その処理を効率化できればSATソルバの高速化が可能となる． 本論文では，「$n$個の変数のうち，ちょうど$k$個が真」という基本対称関数を導入することにより入力する論理式の大きさが減少することに注目し，SATソルバの効率化を目指す． 実際にSATソルバでよく用いられるDLLアルゴリズムを基本対称関数を持つCNFに拡張し，その有効性を実験により確かめた． |
| （英） | In recent years, several efficient SAT solvers, which decide satisfiability of boolean formulas, have been developed. Since BCP module, which propagates variable values in succession, often consumes most of running time of SAT solvers, the total efficiency will be improved if we succeed in reducing the process of BCP. In this paper, we attempt to improve the efficiency of SAT solvers from the observation that the number of clauses of a CNF formula is decreased by introducing the notion of elementary symmetric functions. We incorporated the notion into the DLL algorithm, implemented a SAT solver based on the extended algorithm and confirmed its effectiveness from experiments. |
|
| キーワード | （和） | SATソルバ / 充足可能性 / 基本対称関数 / 高速化 / / / / |
| （英） | SAT solver / satisfiability / elementary symmetric function / improvement of efficiency / / / / | |
| 文献情報 | 信学技報, vol. 108, no. 362, SS2008-44, pp. 31-36, 2008年12月. | |
| 資料番号 | SS2008-44 | |
| 発行日 | 2008-12-11 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2008-44 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2008-12-18 - 2008-12-19 |
| 開催地（和） | (1日目)高知工科大、（2日目）高知市文化プラザ「かるぽーと」 |
| 開催地（英） | Kochi Univiersity of Technology |
| テーマ（和） | 一般 |
| テーマ（英） | general |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2008-12-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 基本対称関数を付加したCNF論理式の充足可能性判定 |
| サブタイトル（和） | |
| タイトル（英） | Solving Satisfiability of CNF Formulas with Elementary Symmetric Functions |
| サブタイトル（英） | |
| キーワード(1)（和/英） | SATソルバ / SAT solver |
| キーワード(2)（和/英） | 充足可能性 / satisfiability |
| キーワード(3)（和/英） | 基本対称関数 / elementary symmetric function |
| キーワード(4)（和/英） | 高速化 / improvement of efficiency |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 馬野 洋平 / Yohei Umano / ウマノ ヨウヘイ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 酒井 正彦 / Masahiko Sakai / サカイ マサヒコ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 坂部 俊樹 / Toshiki Sakabe / サカベ トシキ |
| 第4著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第5著者 氏名（和/英/ヨミ） | 草刈 圭一朗 / Keiichirou Kusakari / クサカリ ケイイチロウ |
| 第5著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2008-12-19 10:00:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | SS2008-44 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | no.362 |
| ページ範囲 | pp.31-36 |
| ページ数 | 6 |
| 発行日 | 2008-12-11 (SS) |
[研究会発表申込システムのトップページに戻る]