| 研究概要 |
本年度は,SATスケジューリングの高速化と,本研究の基盤となる高速SATソルバの開発・分散協調SATシステムの開発に取り組んだ。
命題論理の充足可能性判定問題(SAT問題)を利用したスケジューリング問題の解法では,複数のSAT問題を次々と解く必要がある。これを高速化するために,これまでSATソルバが学習する「失敗に関する記録」(これを補題と呼ぶ)を再利用する技術を開発してきたが,今年度は新たにSAT問題を充足するモデルを再利用する手法とSAT問題中の仮説を再利用する手法を考案し,その評価を行った。その結果,従来までの手法と比較して約1.6倍高速化できることを確認した。
また本研究では,分散協調SATシステムの開発を平成20年度以降に行う予定であったが,分散環境の整備および開発技術の習得が順調に進んだため,計画を前倒しして本年度から実施した。複数のCPUコアを搭載したPCが普及傾向にあること,またPCの低コスト化を考慮して,MPI(Message Passing Interface)を利用した分散協調SATシステムの開発に取り組んだ。本システムは,(複数のCPUコアを搭載した)1台のPCだけでなく,複数のPCでも動作可能である。システムの構築にあたっては,SAT問題の高速な分割方法の確立,探索失敗の記録である学習節の共有,複数の探索戦略の並列実行,冗長な部分SAT問題の検出などの手法を考案し,実装を行った。7台のPCを用いた予備的な評価実験の結果,約5倍の速度向上が得られることを確認した。しかし,本システムには実装上まだ冗長な点があり,またSAT問題の分割アルゴリズムにも改善の余地があるため,来年度以降さらなる性能向上に継続的に取り組む予定である。
|
