| 研究概要 |
本年度は,(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で準優勝という優れた成績をおさめた
|
