| 演題番号 | 3J1-OS7-8 |
|---|---|
| 題目 | SOLタブロー計算法に基づく命題論理の充足可能性判定器の実現 |
| 著者 | 鈴木 健士郎(山梨大学大学院医学工学総合教育部コンピュータ・メディア工学専攻) 鍋島 英知(山梨大学大学院医学工学総合研究部) |
| 時間 | 06月03日(Fri) 11:25〜11:45 |
| 概要 | 本研究では，命題論理の充足可能性判定(SAT)問題に対し，結論発見手続きSOLタブロー法に基づく新しいソルバを提案する．SOLタブロー法では，充足不能の原因を示す最小の証明木を計算可能であり，また漸次的計算が可能なため，SATソルバのインクリメンタル探索の実現に向くなどの特徴がある．本研究ではSOLタブロー法に最新のSATソルバ技術を導入することで，高速なSATソルバの実現を図る． |
| 論文 | PDFファイル |