2009 Fiscal Year Annual Research Report
大規模SAT問題解決のためのEPRプルーバに関する研究
| Project/Area Number |
21300054
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
長谷川 隆三 Kyushu University, 大学院・システム情報科学研究院, 教授 (20274483)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
藤田 博 九州大学, 大学院・システム情報科学研究院, 准教授 (70284552)
越村 三幸 九州大学, 大学院・システム情報科学研究院, 助教 (30274492)
力 規晃 徳山工業高等專門学校, 情報電子工学科, 助手 (50290804)
|
|---|
| Keywords | SATソルバー / EPR論理 / モデル生成法 / 並列分散処理 |
|---|
| Research Abstract |
本年度は,(A)MiniMG(MM-MGTPの命題特化版)と(B)問題分割方式の分散型並列ソルバーについて研究を進め,1件の査読付論文の公表,4件の学会発表を行った.
(A)では、得られた極小モデルから,非極小枝を刈り込むための負節を生成するモデル制約(MC)方式と,モデルが得られる度に,その極小性テストを行う根拠検査(GT)方式の二種を作成した.SATベンチマークに対する予備実験では,MiniMGは,Industry問題の一部を除きMGTPを凌駕し,また,random問題を除きMinisatを凌駕するという結果が得られた.さらに,極小モデル数が大規模になるにつれて,GT方式がMC方式を凌駕することが判明した.
(B)では,ジョブショップスケジューリング問題について,UB-LB個(UBは上限,LBは下限)個のSATインスタンスを生成し,それぞれを並列に解くことによって,未解決問題を2題解くことに成功した.また,凖群の存在問題のQG5と呼ばれる問題を256個の部分問題に分割し,それぞれを並列にSATソルバで解くことにより,次数18の場合には,解がないことを世界で初めて明らかにした.
定期的な研究活動については,力研究分担者が月1回程度,九州大学を訪問し,成果発表・研究交流・情報交換を行った.
|
Research Products
(6 results)
