さらに、より多くの配列を一度に、実用的な時間内でアライメントすることを可能にする限定分割手法も、同時に開発した。これは、上記の並列反復改善法を用いた実験結果を調査し、各反復ごとに選ばれたアライメントがどのように分割されていたかに注目することで得られた。2つのグループに分割する際に、片方を少ない本数にすると効果的な改善が行われるのである。この手法を並列反復改善法に組込むことで、実際に生物分野で扱われるような多くの本数の配列群を同時に扱っても、高品質なアライメントを妥当な時間内で獲得できる。
デモンストレーション
今回のデモンストレーションでは、並列反復改善法を用いて、一度に22本のアミノ酸配列群のアライメントを行う。256の要素プロセッサ(PE)をもつPIM/n上で実行を行い、約10分で終了する。
なお、分割限定法(今回は、少ない方の配列群を1本、もしくは2本の場合のみに限定)を適用し、すべての分割に対して、2次元DPを並列に実行するために253PEを使用している。また、各反復ごとに最良のアライメントを選択するために1PEを使用しているため、実際には254PEを稼働させている。
このデモンストレーションでは、反復を繰返すたびに、アライメントが改善されてゆく様子がわかりやすく表示される(図5参照)。それぞれの文字は、そのアミノ酸のもつ性質に従って配色を行っている。また、アライメントの下に、各カラムごとのスコアを棒グラフを用いて図示している。これは、棒が高いほど、そのカラムに性質の良く似たアミノ酸が並べられていることを意味している。特に良く似たアミノ酸がたくさん並んでいる部分は、進化の過程において保存された部分だと考えられ、タンパク質の構造や機能の点で重要な意味を持つ、配列モチーフである可能性が高い。このデモンストレーションの最終結果では、ATPに結合する機能をもつ配列モチーフを捕えることに成功している。
並列自動証明システムMGTP
概要
本研究では並列推論マシンPIM/m上の並列推論システムの開発を行なっている。現在ICOTでは、以下の2点を達成することを目標として、モデル生成法に基づいた定理証明系MGTPの研究開発を進めている。
1.ロジックプログラミングと自動推論技術の結合及び並列推論マシンにおける並列処理技術の開発により、1階述語論理の高速定理証明系を実現する。
2.知的データベース、仮説推論システム、自然言語処理や自動プログラミングなどの分野に応用可能な先進的な推論エンジンを提供する。
特徴
●KL1の節コンパイル技術の応用とメタプログラミング機能の開発により、効率的な定理証明系を実現
●高スケーラビリティを実現するAND/0R並列処理技術の開発により、PIM/m(256台)上において線形台数効果を達成
●定理証明系の開発実験環境を構築
●MGTPの応用研究(仕様記述,アブダクション、自動プログラミング)
モデル生成法：
与えられた節集合から前向きに単位節(モデル)を生成する
間題例:
(a)Party問題　　・非ホーン基底問題
(b)Condense Detachment問題
・ホーン非基底問題
・群論、環論、含意論理
MGTPの並列化
MGTPによる証明過程では以下のプロセスに並列性が存在している。
●場合分け
●節の前件部の連言照合
●包摂テスト
これらのプロセスに関して、場合分けにおけるOR並列性と節前件部の連言照合や包摂テストにおけるAND並列性に着目し、MGTPの並列化を行なった。
OR並列化
非ホーン基底問題に対しては、場合分けによるOR並列化が有効であることから、MERC方式に基づいたOR並列MGTPを開発した。プロセス割り付け方式は、証明過程の際に発生するOR並列のプロセスフォークを、プログラム資源の要件を満たすように制限した、'制限付きOR'並列化に基づいたものである。この並列化を実現するため、深さ制限割り当て方式と呼ばれるプロセス割り付け方式を開発した。この方式では、マスタプロセッサが利用可能なスレーブプロセッサ数を越えるまでモデル候補を生成し、ある探索木のレベルで越えた時点で、スレーブプロセッサに残りのタスク(探索木の枝)を割り当てる。各スレーブプロセッサは割り当てられた探索木の枝の探索だけを行ない、他のプロセッサにはタスクを投げない。この方式では、プロセッサ間の通信が非常に小さいので、負荷分散が極めて有効に働く。
AND並列化
連言照合と包摂テストの並列化によって、ホーン問題に対するAND並列化を行い、遅延モデル生成に基づいてMGTPの並列化を実現した。本システムでは、PE台数によって証明が変わらない証明不変方式、(分散メモリアーキテクチャ上で各PEが全モデルをコピーして持つ)モデル共有方式、マスター・スレーブ方式を採用した。
証明不変　並列定理証明器を開発する際の我々の方針は、得られた速度向上が並列化によるものなのか、戦略による探索空間の刈り込みによるものなのか、を明確に区別することである。証明変動方式においてPE台数を変えることは戦略を変えることになり、それによって超線形台数効果が得られることもあれば、逆に証明が長びいたりすることもある。これに対し証明不変方式では台数によって証明が変わらないので、投入したPE台数に見合った速度向上を得ることが可能である。
モデル共有　モデル共有方式の利点は、連言照合や包摂テストといった最もコストのかかる計算を他のPEと独立に最小のPE問通信で行えることである。
マスター・スレーブ　マスター・スレーブ方式では、逐次版MGTPをスレーブPE上に置き、単にそれらとマスタPEとつなぐことによって簡単に並列システムを構築することができる。スレーブプロセスは、暇になるとマスタプロセスからタスクを受けとれ、また各タスクの粒度はほぼ均等なので、良い負荷分散が得られる。
本システムでは、生成プロセスと包摂プロセスは要求駆動方式、棄却プロセスはデータ駆動方式で走行する。
本システムにおいて、並列化の際の最も大きな阻害要因は、包摂テストの逐次性である。この逐次性は、KL1の同期機構によって最小に抑えることができる。
また、KL1のストリームを利用して、要求駆動制御が容易にかつ効率良く実現することができる。
要求駆動制御により、不必要なモデル拡張や包摂テストを抑制でき、さらに高い稼働率を得ることができる。高稼働率の達成は線形台数効果を得るためには必須である。