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ファイル |