Recent Advances in SAT Solvers and their Utilization Technologies.
Recent Advances in SAT Solvers and their Utilization Technologies.
复制标题
SAT 求解器及其应用技术的最新进展。
DOI：
10.11309/jssst.35.72
复制
发表时间：
2018
影响因子：
--
通讯作者：
鍋島 英知
中科院分区：
文献类型：
--
作者：
宋 剛秀;番原 睦則;田村 直之;鍋島 英知
命題論理式の充足可能性判定 (SAT) 問題を解くプログラムである SAT ソルバーは, 2000 年以降その性能面において飛躍的に進化した. それに伴い, 解きたい問題を SAT 符号化により SAT 問題へと変換し, SAT ソルバーを用いて解く SAT 型システムが, プランニング, ソフトウェア・ハードウェア検証, スケジューリング問題など様々な分野で成功を収めるようになった. 本稿では, まず SAT ソルバーの最新動向として, 性能面と機能面における進化をその要因の 1 つである SAT ソルバーの国際競技会の視点から説明を行う. 次に SAT ソルバーの利用技術の視点から, SAT ソルバーの機能面の進化と符号化技術を組み合わせることで, 複雑な問題を解くことが可能になることの説明を行う. そのような例として多目的最適化問題のパレート解を SAT ソルバーを利用して求める方法を説明する.