| 演題番号 | 3J1-OS7-4 |
|---|---|
| 題目 | 基数制約の概念を持つSATソルバの設計と評価 |
| 著者 | 山根 裕二(早稲田大学理工学術院情報理工学科) 徐 暁雋(早稲田大学理工学術院情報理工学科) 上田 和紀(早稲田大学理工学術院情報理工学科) |
| 時間 | 06月03日(Fri) 09:50〜10:10 |
| 概要 | 実問題から生成される構造的な問題に含まれる基数制約は，真理値のみを扱うSAT ソルバにとってボトルネックとなる．そこで，基数制約を表し高速な伝播が可能な特殊節を加えた拡張CNF を提案する．標準的なSAT ソルバのMiniSat2.0 の推論フェーズと衝突による学習フェーズを改訂し特殊節に対応させ，基数制約を含む時間割作成問題をベンチマークとして従来のMiniSat2.0 との比較実験を行った． |
| 論文 | PDFファイル |