文章基本信息

标题：インクリメンタルSAT解法ライブラリとその応用
本地全文：下载
作者：迫龍哉 ; 宋剛秀 ; 番原睦則等
期刊名称：コンピュータソフトウェア
印刷版ISSN：0289-6540
出版年度：2016
卷号：33
期号：4
页码：4_16-4_29
DOI：10.11309/jssst.33.4_16
出版社：Japan Society for Software Science and Technology
摘要：近年，命題論理の充足可能性判定(SAT)問題を解くSATソルバーの飛躍的な性能向上を背景に，問題をSATに変換し，SATソルバーを用いて求解するSAT型ソルバーが成功を収めている．しかしながら，最適化問題，解列挙問題などに対しては，SATソルバーを複数回起動する必要があり，求解性能が大きく低下することがある．この問題を解決する方法として，インクリメンタルSAT解法の利用が挙げられる．SATソルバー競技会のひとつであるSAT Race 2015で，このような解法を容易に実現するためのインクリメンタルSAT APIが提案された．本論文では，それを拡張したインクリメンタルSAT APIであるiSATを提案し，その応用について述べる．提案する拡張により，問題を簡潔に記述でき，Javaからの利用も可能になる．また，ショップスケジューリング問題，N-クイーン問題，ハミルトン閉路問題に対する実験結果を通じ，iSAT利用の有効性を示す．