文献

J-GLOBAL ID：201502215990205058   整理番号：15A1192330

iSugar:インクリメンタルSAT解法が利用可能なSAT型制約ソルバー

著者 (6件)： 迫龍哉 (神戸大 大学院システム情報学研究科) ,  宋剛秀 (神戸大 情報基盤セ) ,  番原睦則 (神戸大 情報基盤セ) ,  田村直之 (神戸大 情報基盤セ) ,  鍋島英知 (山梨大 大学院医学工学総合研究部) ,  井上克巳 (国立情報学研)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 32nd  ページ： ROMBUNNO.PPL6-1  発行年： 2015年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 近年,命題論理の充足可能性判定(SAT)問題を解くSATソルバーの飛躍的な性能向上を背景に,制約充足問題をSATに変換し,SATソルバーを用いて求解するSAT型制約ソルバーが成功を収めている。しかしながら,制約最適化問題,解列挙問題などに対しては,SATソルバーを複数回起動する必要があり,求解性能が大きく低下することがある。この問題を解決する方法として,インクリメンタルSAT解法の利用が挙げられる。SAT Race2015で,このような解法を容易に実現するためのインクリメンタルSAT APIが提案された。本稿では,インクリメンタルSAT APIの拡張と,これに対応したインクリメンタルSAT型制約ソルバーを提案する。提案システムの実現として,iSugarを開発した。iSugarの特長は,上記の求解困難な問題に対して,ただ一度だけSATソルバーを起動し,かつ学習節を再利用することにより,求解性能を大きく向上できる点である。実験の結果,ショップスケジューリング問題,N-クイーン問題,ハミルトン閉路問題に対して,iSugarの有効性を確認した。(著者抄録)

シソーラス用語： *充足可能性問題 ,  *制約付最適化問題 ,  アルゴリズム ,  逐次近似 ,  応用プログラム ,  命題論理 ,  性能評価 ,  システムインタフェイス ,  ソフトウェア設計 ,  ジョブショップスケジューリング
準シソーラス用語： *制約最適化問題 ,  インクリメンタルアルゴリズム ,  ソルバ ,  API【計算機】

分類 (2件)： 論理代数  (JB03000H) ,  オペレーションズリサーチの基礎的数学理論  (KA03020B)

タイトルに関連する用語 (4件)： SAT ,  解法 ,  制約 ,  ソルバー