インクリメンタルSAT解法ライブラリとその応用

• 迫 龍哉

  神戸大学大学院システム情報学研究科

• 宋 剛秀

  神戸大学情報基盤センター

• 番原 睦則

  神戸大学情報基盤センター

• 田村 直之

  神戸大学情報基盤センター

• 鍋島 英知

  山梨大学大学院医学工学総合研究部

• 井上 克巳

  国立情報学研究所情報学プリンシプル研究系 総合研究大学院大学複合科学研究科情報学専攻 東京工業大学大学院情報理工学研究科計算工学専攻

書誌事項

タイトル別名

• 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

  日本ソフトウェア科学会

詳細情報

• CRID: 1390001204736535168
• NII論文ID: 130005290581
• NII書誌ID: AN10075819
• DOI: 10.11309/jssst.33.4_16
• NDL書誌ID: 027737439
• ISSN: 02896540
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I027737439
• 本文言語コード: ja
• データソース種別:
  • JaLC
  • NDL
  • CiNii Articles
  • KAKEN
• 抄録ライセンスフラグ: 使用不可