2010 Fiscal Year Annual Research Report
大規模SAT問題解決のためのEPRプルーバーに関する研究
| Project/Area Number |
21300054
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
長谷川 隆三 九州大学, システム情報科学研究院, 教授 (20274483)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
藤田 博 九州大学, システム情報科学研究院, 准教授 (70284552)
越村 三幸 九州大学, システム情報科学研究院, 助教 (30274492)
力 規晃 徳山工業高等専門学校, 情報電子工学科, 助手 (50290804)
|
|---|
| Keywords | モデル生成 / SAT / MaxSAT / 分散処理・並列処 |
|---|
| Research Abstract |
本年度は,(A)モデル生成型SATソルバーMiniMGの探索領域削減手法,(B)基数制約を用いたMaxSATソルバー,(C)抽象モデル生成によるSAT問題の前処理,(D)Unixのfork機能に基づくSATソルバーの並列化,(E)分散処理フレームワークHadoopによるSATソルバーの並列化について研究を進め,3件の査読付論文の公表,5件の学会発表を行った
以下,(A)～(E)のあらましを述べる
(A)学習節の評価尺度の一つであるLBD (Literals Blocks Distance)に基づく学習節の削除手法とリスタート戦略により探索空間を削減することに成功した
(B)SATの拡張であるMaxSATのソルバーを,基数制約のCNF符号化を利用して作成した
(C)一階CNFの前処理手法である抽象モデルによる前処理をSAT問題に適用しその効果を実証した
(D)数千ノードでの処理も可能なHadoopを用いてSATソルバーの並列化を行った.2ノードを用いた実験により,性能向上の見通しが得られた
(E)Unix環境下でプロセスの複製が容易に行えるfork機能を用いてSATソルバーの並列化を行った.16コアマシン上でのベンチマーク100題の実験では,逐次版に比べ解けた問題数が6題増加した
本研究の研究成果の一つであるMaxSATソルバーQMaxSATは,MaxSAT Evaluationに参加し,Partial MaxSAT部門において,参加した全13ソルバー中Industrialで優勝,Craftedで準優勝という優れた成績をおさめた
|
