05月12日(Mon) 15:20〜17:00 D会場(48人-ひめぎんホール 第3会議室)
| 演題番号 | 1D4-OS-11a-1 |
|---|---|
| 題目 | 極小モデル生成とMaxSATソルバーについて |
| 著者 | 長谷川 隆三(九州大学大学院システム情報科学研究院情報学部門) |
| 時間 | 05月12日(Mon) 15:20〜16:00 |
| 概要 | モデル生成法とDPLL法の２つの証明手法の特徴を踏まえて、各手法による極小モデル生成 の実現法を紹介する。１階のモデル生成器MGTPを命題に特化したMiniMGとDPLL型SATソルバーMiniSATの性能比較を行う。制約充足問題は基数制約を付加してSAT問題に変換して解くことができる。代表的な基数制約の符号化方式Totalizerの改良版を提示し、MaxSAT問題を対象にその性能評価を行う。 |
| 論文 | PDFファイル |