| 講演抄録／キーワード |
| 講演名 |
2006-05-18 11:35
抽象モデルを利用したＳＡＴ問題の前処理
○越村三幸・長谷川隆三（九大） |
| 抄録 |
（和） |
我々は一階の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 propositional CNF formula (SAT problem) and
evaluates its effect for the problems from SATLIB. |
| キーワード |
（和） |
CNF論理式 / 抽象化 / 簡単化 / SAT問題 / / / / |
| （英） |
CNF formula / abstraction / simplification / SAT / / / / |
| 文献情報 |
信学技報, vol. 106, no. 38, AI2006-5, pp. 25-28, 2006年5月. |
| 資料番号 |
AI2006-5 |
| 発行日 |
2006-05-11 (AI) |
| ISSN |
Print edition: ISSN 0913-5685 |
| PDFダウンロード |
|