MGTPの並列化
MGTPによる証明過程では以下のプロセスに並列性が存在している。
これらのプロセスに関して、場合分けにおけるOR並列性と節前件部の連言照合
や包摂テストにおけるAND並列性に着目し、MGTPの並列化を行なった。
OR並列化
非ホーン基底問題に対しては、場合分けによるOR並列化が有効であることか
ら、MERC方式に基づいたOR並列MGTPを開発した。プロセス割り付け方式
は、証明過程の際に発生するOR並列のプロセスフォークを、プログラム資源の
要件を満たすように制限した、'制限付きOR'並列化に基づいたものである。こ
の並列化を実現するため、深さ制限割り当て方式と呼ばれるプロセス割り付け方
式を開発した。この方式では、マスタプロセッサが利用可能なスレーブプロセッ
サ数を越えるまでモデル候補を生成し、ある探索木のレベルで越えた時点で、ス
レーブプロセッサに残りのタスク(探索木の枝)を割り当てる。各スレーブプロセッ
サは割り当てられた探索木の枝の探索だけを行ない、他のプロセッサにはタスク
を投げない。この方式では、プロセッサ間の通信が非常に小さいので、負荷分散
が極めて有効に働く。
深さ制限付き割付け方式 |
- 67 -