文献

J-GLOBAL ID：201602283916619824   整理番号：16A0621848

SAT技術の進化と応用~パズルからプログラム検証まで~5)SATソルバーの最近の進展

著者 (5件)： 鍋島英知 (山梨大) ,  岩沼宏治 (山梨大) ,  井上克巳 (国立情報学研) ,  井上克巳 (総合研究大学院大) ,  井上克巳 (東京工大)
資料名： 情報処理  (IPSJ Magazine)
巻： 57  号： 8  ページ： 724-729  発行年： 2016年07月15日 
JST資料番号： G0427A  ISSN： 0447-8053  資料種別： 逐次刊行物 (A)
記事区分： 解説  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 並列化を中心としてSATソルバーの最近の進展について解説した。SATソルバーにおける最近の流行の1つは並列化である。その背景には,複数のCPUコアを搭載した計算機の普及により,そのリソースを有効活用したいという要望がある。並列SATソルバーでは,複数の逐次SATソルバーを並列実行するのが一般的な手法となっている。従って,逐次SATソルバーは並列SATソルバーの基盤といえる。本稿ではまず,逐次SATソルバーの最近の動向を紹介した。次いで,並列SATソルバーにおける最近の話題として,探索空間を複数に分割して各部分探索空間を並列に解く探索空間分割型並列SATソルバー,および同一の問題を種類の異なるSATソルバーで並行して解くポートフォリオ型並列SATソルバーについて説明した。

シソーラス用語： *充足可能性問題 ,  応用プログラム ,  解法 ,  *並列処理 ,  情報検索 ,  ポートフォリオ
準シソーラス用語： ソルバ ,  探索空間

分類 (1件)： 計算機利用技術一般  (JE01000C)

引用文献 (1件)：

• Balyo, T., Sanders, P. and Sinz, C.: HordeSat : A Massively Parallel Portfolio SAT Solver, In Proceedings of SAT 2015, pp.156-172 (2015).

タイトルに関連する用語 (7件)： SAT ,  進化 ,  応用 ,  パズル ,  プログラム検証 ,  ソルバー ,  進展