06月05日(Wed) 15:00〜17:40 E会場(-国際会議場204号室)
| 演題番号 | 2E4-OS-09a-3 |
|---|---|
| 題目 | 最新SATソルバーへの充足不能コア抽出手法の実装 |
| 著者 | 渡辺 大樹(山梨大学工学部コンピュータ•メディア工学科) 鍋島 英知(山梨大学大学院医学工学総合研究部) |
| 時間 | 06月05日(Wed) 16:00〜16:20 |
| 概要 | 充足不能な命題論理式から，できる限り小さな充足不能な節集合（充足不能コア）を高速に抽出するため，我々は，Shachamらによる導出過程をメモリ上に効率よく保持する手法を，入力節集合や学習節の簡単化手法を備えた最新のSATソルバに実装した．節の簡単化は最新SATソルバの重要な要素技術の1つであり，充足不能コアの高速抽出に必要不可欠な要素である．本稿では簡単化技術を含めた充足不能コアの抽出手法を示す． |
| 論文 | PDFファイル |