| 研究概要 |
本年度は,(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回程度,九州大学を訪問し,成果発表・研究交流・情報交換を行った.
|
