文献

J-GLOBAL ID：201902210053253596   整理番号：19A2085088

プログラミングおよびプログラミング言語 SATソルバーの最新動向と利用技術

Recent Advances in SAT Solvers and their Utilization Technologies.

著者 (4件)： 宋剛秀 (神戸大 情報基盤セ) ,  番原睦則 (神戸大 情報基盤セ) ,  田村直之 (神戸大 情報基盤セ) ,  鍋島英知 (山梨大 大学院医学工学総合研究部)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 35  号： 4  ページ： 72-92(J-STAGE)  発行年： 2018年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 命題論理式の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーは,2000年以降その性能面において飛躍的に進化した.それに伴い,解きたい問題をSAT符号化によりSAT問題へと変換し,SATソルバーを用いて解くSAT型システムが,プランニング,ソブトウェア・ハードウェア検証,スケジューリング問題など様々な分野で成功を収めるようになった.本稿では,まずSATソルバーの最新動向として,性能面と機能面における進化をその要因の1つであるSATソルバーの国際競技会の視点から説明を行う.次にSATソルバーの利用技術の視点から,SATソルバーの機能面の進化と符号化技術を組み合わせることで,複雑な問題を解くことが可能になることの説明を行う.そのような例として多目的最適化問題のパレート解をSATソルバーを利用して求める方法を説明する.(著者抄録)

シソーラス用語： *充足可能性問題 ,  計算機プログラミング ,  符号化 ,  プログラミング言語 ,  *計算量理論 ,  *多目的計画法 ,  *最適条件 ,  *Pareto最適
準シソーラス用語： SAT符号化 ,  最新動向 ,  *多目的最適化問題

分類 (1件)： 計算理論  (JB02000A)

タイトルに関連する用語 (5件)： プログラミング ,  プログラミング言語 ,  SAT ,  ソルバー ,  最新動向