著者

迫 龍哉 宋 剛秀 番原 睦則 田村 直之 鍋島 英知 井上 克巳

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.33, no.4, pp.4_16-4_29, 2016-10-25 (Released:2017-01-14)

---

近年,命題論理の充足可能性判定(SAT)問題を解くSATソルバーの飛躍的な性能向上を背景に,問題をSATに変換し,SATソルバーを用いて求解するSAT型ソルバーが成功を収めている.しかしながら,最適化問題,解列挙問題などに対しては,SATソルバーを複数回起動する必要があり,求解性能が大きく低下することがある.この問題を解決する方法として,インクリメンタルSAT解法の利用が挙げられる.SATソルバー競技会のひとつであるSAT Race 2015で,このような解法を容易に実現するためのインクリメンタルSAT APIが提案された.本論文では,それを拡張したインクリメンタルSAT APIであるiSATを提案し,その応用について述べる.提案する拡張により,問題を簡潔に記述でき,Javaからの利用も可能になる.また,ショップスケジューリング問題,N-クイーン問題,ハミルトン閉路問題に対する実験結果を通じ,iSAT利用の有効性を示す.