書誌事項
- タイトル別名
-
- An Incremental SAT Solving Library and its Applications
- インクリメンタル SATカイホウ ライブラリ ト ソノ オウヨウ
この論文をさがす
抄録
近年,命題論理の充足可能性判定(SAT)問題を解くSATソルバーの飛躍的な性能向上を背景に,問題をSATに変換し,SATソルバーを用いて求解するSAT型ソルバーが成功を収めている.しかしながら,最適化問題,解列挙問題などに対しては,SATソルバーを複数回起動する必要があり,求解性能が大きく低下することがある.この問題を解決する方法として,インクリメンタルSAT解法の利用が挙げられる.SATソルバー競技会のひとつであるSAT Race 2015で,このような解法を容易に実現するためのインクリメンタルSAT APIが提案された.本論文では,それを拡張したインクリメンタルSAT APIであるiSATを提案し,その応用について述べる.提案する拡張により,問題を簡潔に記述でき,Javaからの利用も可能になる.また,ショップスケジューリング問題,N-クイーン問題,ハミルトン閉路問題に対する実験結果を通じ,iSAT利用の有効性を示す.
収録刊行物
-
- コンピュータ ソフトウェア
-
コンピュータ ソフトウェア 33 (4), 4_16-4_29, 2016
日本ソフトウェア科学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1390001204736535168
-
- NII論文ID
- 130005290581
-
- NII書誌ID
- AN10075819
-
- NDL書誌ID
- 027737439
-
- ISSN
- 02896540
-
- 本文言語コード
- ja
-
- データソース種別
-
- JaLC
- NDL
- CiNii Articles
- KAKEN
-
- 抄録ライセンスフラグ
- 使用不可