問題の構造を利用した高速並列SATソルバの研究開発

2016 年度 研究成果報告書

• 研究課題/領域番号: 15K16057
• 研究種目: 若手研究(B)
• 配分区分: 基金
• 研究分野: 知能情報学
• 研究機関: 国立情報学研究所
• 研究代表者: 薗部 知大 国立情報学研究所, ビッグデータ数理国際研究センター, 特任研究員 (50747269)
• 研究期間 (年度): 2015-04-01 – 2017-03-31
• キーワード: 充足可能性問題 / SATソルバ / 探索 / 並列 / グラフ

研究成果の概要

充足可能性問題(SAT問題)は効率的に解くのが難しいと信じられている問題であるが、ソフトウェアや論理回路の検証等を行う際に使用される。そのため、この問題を解くSATソルバの高速化の意義は高く、本研究課題では大規模な問題を処理するための高速並列SATソルバを、グラフ理論の手法を用いて研究開発を行った。作成した並列ソルバは、SATソルバの性能を競う国際的な競技会で上位に入賞を果たし、その性能の高さを示した。

自由記述の分野

SATソルバ