したがって、上では、探索は、1から14の順に 行われることになる。
最終的な証明木が、極端な非対称形ではない場合でかつ全解探索が必要とされる ような問題においては、縦型探索、横型探索の間に効率上の際は生じない。 しかし、拡張を繰り返す特別な枝を持つような問題で、かつ単解のみが求められる 問題においては、深さ優先の縦型探索はしばしば非効率的になるだけでなく、 無限に枝を拡張するような枝を深さ優先で探索する場合には、結果が返ってこない 場合がある。
たとえば、上の例で、b が求めるべきものであるとすれば、縦型探索では、 左側の枝がすべて閉じてから bを含む枝を探索するので、第9ステップ目に はじめて b に到達するのに対して、幅優先の横型探索では、5ステップ目に b に到達することができる(以下、図参照)。
以下では、複数の探索ポイントとして MGTP が保持する モデル候補の集合を定量的に評価し、その評価値にしたがって 探索ポイントの制御をを分岐限定法をベースにしたアルゴリズムに したがって行う方法を説明する。
【評価方式の例】
評価は、各モデル候補に対する選好を数量化したもので、一般に問題依存である。
ここでは、一般的な方法として、
「モデル候補を生成するに至った推論ステップ数」を
モデル候補の評価値と考える。
すなわち、モデル拡張節をピックアップし、連言照合を行った時点で
評価値をインクリメントする。
ただし、dom 述語に関しては、いわば領域定義のための拡張であり、
証明木全体のコストとは関係しないので、dom 述語のピックアップに
関してはインクリメントを行わない。
また、ゴール(充足可能)に至ったモデル候補の中で、最小の評価値を持つものを データとして保持しておく。これは分岐限定法に基づいて探索ポイントの制御 を行う際に必要になる。 最小値更新の手続きを以下に示す。
本機能では、深さ優先に基づく基本推論機能の探索戦略を補うことを目的として、 前節「モデル候補評価機能」によって管理される探索コストを基にして探索の 制御を行う。
探索の制御は、分岐限定法による例を説明する。 分岐限定法は、最良優先探索と同様、その時点で最も評価値の高い枝を分岐 (展開)させていくが、ゴールに至るコスト最小値を保持し、これを越えない限り 探索ポインタを破棄せず、可能性として残しておくという点が異なる。 これにより、最良優先探索の不完全性(すなわち、最適解に至ることが保証されない) 点を補い、最適解に至ることが保証されている。 最良優先探索による証明木を下に示す。 ここで、細数字は評価値を、また太数字は探索順を示すものである。 この例では、本来最適解に至るべきノードが探索されなかったことがわかる。
●分岐スタックコントロール
MGTPでは、分岐が生じたときのモデル候補、モデル拡張候補 (単位節バッファ、選言バッファ、dom述語バッファ)、項メモリの アクティブセル情報は、スタックとして管理されている。 探索ポインタの制御は、このスタックを参照して、適当な要素を選び出し、 カレントの情報にポインタをつけかえることによって実現することができる。
●最小コストを持つモデル候補の選択
分岐スタックをもとに最小コストを持つ探索ポインタを選択する手続きが必要である。 具体的には、スタックの個別要素ごとに、モデル候補評価機能を参照して、 評価値を得て、現在までの最小値と比較を行う。 スタックが NULL になったときに、最小値として保持されている値が、 得られた最小値であり、そのときのスタック要素が、次に選択すべき 探索ポインタである。
●ポインタの変更
選択された分岐スタックの要素から、モデル候補、モデル拡張候補 (単位節バッファ、選言バッファ、dom述語バッファ)、項メモリの アクティブセル情報を取りだし、カレントの変数へ代入を行う。
● 最小コストによるモデル候補の棄却
分岐が最終的に sat (充足可能)に到達したときには、そのコストを mincost として保存する。 もし、分岐スタックに対して、コスト計算をする際に、この mincost を 越えるものがあれば、ただちにその枝の探索を終了する。 具体的には、cancelled branch として closed フラグを ON にする。 cancelled branch は、統計情報としてブランチ数をカウントして、 証明終了時に統計情報として出力する。
以上の処理の流れを図に表すと以下の図のようになる。