| 講演名 | 2006-05-18 抽象モデルを利用したSAT問題の前処理(「自動化:推論,発見,学習,データマイニング」及び一般) 越村 三幸, 長谷川 隆三, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 我々は一階のCNF論理式に対する抽象化を考案し,このエルブランモデルを用いて元のCNF式を簡単化(前処理)する方式を提案している.簡単化することによって,一階の定理証明システムの負荷を軽減することを狙っている.本稿では,この方式を命題のCNF論理式(SAT問題)に適用した効果について報告する. |
| 抄録(英) | We presented an simplification (pre-processing) method for the first-order CNF formula. The method makes use of an abstraction of the formula. We aimed to enhance the performance of automated theorem provers with the method. This paper applies the method to the prepositional CNF formula (SAT problem) and evaluates its effect for the problems from SATLIB. |
| キーワード(和) | CNF論理式 / 抽象化 / 簡単化 / SAT問題 |
| キーワード(英) | CNF formula / abstraction / simplification / SAT |
| 資料番号 | AI2006-5 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 2006/5/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 抽象モデルを利用したSAT問題の前処理(「自動化:推論,発見,学習,データマイニング」及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Preprocessing SAT Problems with Abstract Models |
| サブタイトル（和） | |
| キーワード(1)（和/英） | CNF論理式 / CNF formula |
| キーワード(2)（和/英） | 抽象化 / abstraction |
| キーワード(3)（和/英） | 簡単化 / simplification |
| キーワード(4)（和/英） | SAT問題 / SAT |
| 第 1 著者 氏名（和/英） | 越村 三幸 / Miyuki KOSHIMURA |
| 第 1 著者 所属（和/英） | 九州大学大学院システム情報科学研究院 Graduate School of Information Science and Electrical Engineering, Kyushu University |
| 第 2 著者 氏名（和/英） | 長谷川 隆三 / Ryuzo HASEGAWA |
| 第 2 著者 所属（和/英） | 九州大学大学院システム情報科学研究院 Graduate School of Information Science and Electrical Engineering, Kyushu University |
| 発表年月日 | 2006-05-18 |
| 資料番号 | AI2006-5 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 38 |
| ページ範囲 | pp.- |
| ページ数 | 4 |
| 発行日 | |