文献

J-GLOBAL ID：201002209724609367   整理番号：10A0057002

最近のSAT技術の発展 SATソルバーの基礎

著者 (3件)： 井上克巳 (国立情報学研) ,  井上克巳 (総合研究大学院大) ,  田村直之 (神戸大 学術情報基盤セ)
資料名： 人工知能学会誌  (Journal of the Japanese Society for Artificial Intelligence)
巻： 25  号： 1  ページ： 57-67  発行年： 2010年01月01日 
JST資料番号： X0330A  ISSN： 0912-8085  資料種別： 逐次刊行物 (A)
記事区分： 解説  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： ブール式または命題論理式の充足可能性(SAT)を解くための代表的なソルバーとして,1)系統的ソルバー,2)確率的ソルバーがある。本論文では,系統的探索を行う完全なアルゴリズムに基づく1)の基本であるDPLLと,その単位伝播を効率化するための監視リテラル及び矛盾解析を利用したSATソルバーChaffを解説した。次に,確率的局所探索を行う不完全なアルゴリズムに基づく2)として,混合ランダムウォーク戦略を使って局所解から脱出するWalksatや,ランダムSAT問題に適用されるサーベイ伝播について述べた。SATソルバーを実用面で評価するSAT競技会ではポートフォリオ型のSATzillaが平均的な強みを見せたほか,ランダムSATでは2)の進歩が見られた。さらに,SATソルバーの応用として,i)制約充足問題,ii)制約最適化問題,iii)プランニング,スケジューリング,iv)様相論理式,v)擬似ブール制約,vi)一階述語論理式,vii)算術式・データ構造・背景理論,viii)解集合プログラミング,ix)解の列挙,x)確からしさの付与,xi)限定ブール式を命題論理表現に帰着させるためのSAT符号化に関する取組みについて述べた。

シソーラス用語： *充足可能性問題 ,  Boole代数 ,  命題論理 ,  *探索問題 ,  近傍探索法 ,  アルゴリズム ,  酔歩 ,  制約付最適化問題 ,  プランニング【AI】 ,  スケジューリング ,  様相論理 ,  述語論理
準シソーラス用語： ランダムウォーク ,  局所探索 ,  *探索アルゴリズム

分類 (2件)： 論理代数  (JB03000H) ,  人工知能  (JE08000Z)

タイトルに関連する用語 (4件)： SAT ,  発展 ,  ソルバー ,  基礎