AND並列化 連言照合と包摂テストの並列化によって、ホーン問題に対するAND並列化 を行い、遅延モデル生成に基づいてMGTPの並列化を実現した。本システムで は、PE台数によって証明が変わらない証明不変方式、(分散メモリアーキテク チャ上で各PEが全モデルをコピーして持つ)モデル共有方式、マスター・スレー ブ方式を採用した。 証明不変 並列定理証明器を開発する際の我々の方針は、得られた速度向上が並列 化によるものなのか、戦略による探索空間の刈り込みによるものなのか、を 明確に区別することである。証明変動方式においてPE台数を変えることは 戦略を変えることになり、それによって超線形台数効果が得られることもあ れば、逆に証明が長びいたりすることもある。これに対し証明不変方式では 台数によって証明が変わらないので、投入したPE台数に見合った速度向上 を得ることが可能である。 モデル共有 モデル共有方式の利点は、連言照合や包摂テストといった最もコスト のかかる計算を他のPEと独立に最小のPE問通信で行えることである。 マスター・スレーブ マスター・スレーブ方式では、逐次版MGTPをスレーブ PE上に置き、単にそれらとマスタPEとつなぐことによって簡単に並列シ ステムを構築することができる。スレーブプロセスは、暇になるとマスタプ ロセスからタスクを受けとれ、また各タスクの粒度はほぼ均等なので、良い 負荷分散が得られる。 本システムでは、生成プロセスと包摂プロセスは要求駆動方式、棄却プロセス はデータ駆動方式で走行する。 本システムにおいて、並列化の際の最も大きな阻害要因は、包摂テストの逐次 性である。この逐次性は、KL1の同期機構によって最小に抑えることができる。 また、KL1のストリームを利用して、要求駆動制御が容易にかつ効率良く実現す ることができる。 要求駆動制御により、不必要なモデル拡張や包摂テストを抑制でき、さらに高 い稼働率を得ることができる。高稼働率の達成は線形台数効果を得るためには必 須である。 - 69 -