研究室概要 / 研究報告 / 梶江俊之

HOME 研究室概要 コラム 周辺探索 メンバー 掲示板 リンク

ボトムアップ定理証明器における負節拡張アルゴリズムに関する研究

『平成11年度卒業論文(2000)』より

梶江俊之

 目次

1. はじめに
2. モデルの生成法
3. 基本アルゴリズムの問題点と解決策
4. 制限付き負節拡張アルゴリズム
5. Add_TSの動作
6. Add_TSの動作例
7. 比較実験
8. 入力節集合
9. 負節拡張回数の制限
10. 比較結果
11. 現在の取り組み
12. 参考文献

 1. はじめに

 前向きに仮定から目標へと進む推論をボトムアップ(前向き)推論、後向きに目標から部分目標へと進む推論をトップダウン(後向き)推論と言います。

 本研究ではモデル生成法に基づいたボトムアップ推論にトップダウン的な操作を組み合わせることによって、アトムの照合回数を削減し、計算量と必要なメモリ空間の削減を図ります。

 2. モデルの生成法

 モデル生成法とは与えられた節集合のモデルを前向き推論によって機械的に求める証明手法であり、入力節は次の含意形式で与えられます。

A 1 , , A nC 1 | … | C m

 節の種類には

  ●正節 : 前件部が空の節 (trueAnimal (man ))
  ●負節 : 後件部が空の節 (Die (X ) → false )
  ●混合節 : それ以外の節 (Animal (X ) → Die (X ))

の3種類があります。

 モデル生成法は次の2つの操作を繰り返し行います。

  ● モデル棄却操作
モデル候補M に対して、負節

A 1 , , A nfalse

と置換σが存在して、アトムA 1σ, , A nσがすべてのM によって充足されるならば、モデル候補M を棄却する。
  ● モデル拡張操作
モデル候補M に対して、正節あるいは混合節

A 1 , , A nC 1 | … | C m

と置換σが存在して、A 1σ, , A nσがすべてのM によって充足され、かつ、どのC 1, , C mM によって充足しないならば、各C 1σ, , C mσをM に付け加えたm 個のモデル候補を生成する。

 3. 基本アルゴリズムの問題点と解決策

 モデル生成法で入力節をホーン節に限定したアルゴリズムを基本アルゴリズムとします。基本アルゴリズムにおいて爆発的にモデル候補アトムが増加する問題ではアトムの照合回数が増大し、計算量の増大に伴い実行時間が増加します。

 そこで解決策として、負節拡張(トップダウン的)操作を基本アルゴリズムに組み込むことで早い段階で棄却テストを成功させ、アトムの照合回数を減少し、実行時間の減少を図ります。

 4. 制限付き負節拡張アルゴリズム

 制限付き負節拡張アルゴリズムとは基本アルゴリズムに負節拡張操作(Add_TS)を付加したアルゴリズムです。ここでいう制限とは負節拡張操作を行う回数の制限です。下にアルゴリズムを示します。

  TS := {A 1, , A nfalse | (A 1, , A nfalse ) ∈ a set of given clauses};
  GS := {A 1, , A nC | (A 1, , A nC ) ∈ a set of given clauses};
  M :=φ;
  D :={C | (trueC ) ∈ a set of given clauses};
  while D ≠ φ do begin
    select,D ); D := D - Δ;
    if CJMTS,M ) ∋ false …… モデル棄却操作
      then return(unsatisfiable);
    new := CJMGS,M ); …… モデル拡張操作
    M := M ∪ Δ;
    new ’ := subsTest (new , MD );
    D := Dnew ’;
    TS := Add_TS (TS , GS ); …… 負節拡張操作
  end return(satisfiable).

 5. Add_TSの動作

 Add_TSの動作を次に示します。

  Add_TS (TS , GS ) := { (A 1σ, , A i-1σ, A i+1σ, , A nσ ,
B 1σ, , B mσ → false ) ∈ TS |
(A 1, , A nfalse ) ∈ TS
∧ (B 1, , B mC ) ∈ GS
∧ ∃i (i = 1, , n ) A iσ = C σ }

 負節:A 1, , A nfalse と混合節:B 1, , B mC が存在するとき、それぞれに同一の置換σを行うと、A 1σ, , A nσ → falseB 1σ, , B mσ → Cσ が得られます。このとき A iσ = Cσ が存在すれば、A 1σ, , A i-1σ, A i+1σ, , A nσ , B 1σ, , B mσ → false を負節集合に加えます。

 6. Add_TSの動作例

  A (X , Y ) , B (X , Y ) → C (X , Y )
  C (a , b ) → false
(X , Y : 変数 , a , b : 定数)

 上のような節が存在するとき、置換(a / X , b / Y )によりC (X , Y )とC (a , b )の単一化に成功し、A (a , b ) , B (a , b ) → false を生成します。生成後の棄却テスト時にA (a , b ) , B (a , b )が照合に成功すればモデル候補を棄却します。

 7. 比較実験

 図.1の左の状態から右の状態に遷移できるか、という問題で比較実験をおこないました。



図.1: 8パズル

 使用した述語を下に示します。

  State (X 1 , X 2 , X 3 , X 4 , X 5 , X 6 , X 7 , X 8 , X 9)
  Up (X ) : X の番号のコマを上に動かす
  Down (X ) : X の番号のコマを下に動かす
  Right (X ) : X の番号のコマを右に動かす
  Left (X ) : X の番号のコマを左に動かす

 8. 入力節集合

 前に示した述語を用いて、この問題を記述すると次のような節集合が得られます。

  trueState (1 , 6 , 2 , 4 , s , 3 , 7 , 5 , 8)
  trueUp (X )
  trueDown (X )
  trueRight (X )
  trueLeft (X )
  Left (X 2) , State (s , X 2 , X 3 , X 4 , X 5 , X 6 , X 7 , X 8 , X 9)
      → State (X 2 , s , X 3 , X 4 , X 5 , X 6 , X 7 , X 8 , X 9)
  Up (X 4) , State (s , X 2 , X 3 , X 4 , X 5 , X 6 , X 7 , X 8 , X 9)
      → State (X 4 , X 2 , X 3 , s , X 5 , X 6 , X 7 , X 8 , X 9)


  State (1 , 2 , 3 , 4 , 5 , 6 , 7 , 8 , s ) → false

 9. 負節拡張回数の制限

 負節拡張回数αはα回だけ負節拡張を行うように制限していることを表します。(但し、α=0 のときは従来法とする)

 αを設定することにより負節の拡張回数を制限する理由は、際限なく負節拡張を行うより、適度なところで負節拡張をとめた方が効率がよいであろうと考えたからです。

 次にこの制限を加えて負節の数、CPU使用時間、アトムの照合回数を調べた結果を示します。

 10. 比較結果



 アトムの照合回数 (回)


 CPU使用時間 (ミリ秒)

図.2: 比較結果

 比較結果(図.2)から次のことが言えます。

  ● 負節拡張を行うことでアトムの照合回数を削減できた。
  ● 多量の負節の生成によりCPU使用時間が増加するという傾向がみられる。
  ● 従来法と比較した結果CPU使用時間を約10〜40%に抑えることができた。

 11. 現在の取り組み

 現在の研究では非ホーン節を含む問題に対しても負節拡張アルゴリズムを適用し、有効であるかを検証しています。また、ボトムアップ方向とトップダウン方向の負荷を同程度にすることにより証明効率が向上できるかどうか確かめています。

 12. 参考文献

中川智規、泉田正則、村上研二:"ボトムアップ定理証明器における重複照合の削除に関する研究" 平成9年度卒業論文 1998年.

ページの上へ 前の人へ 上のページへ


企画・製作 村上・泉田研究室 HP製作委員会(2001)
ご意見・お問い合わせは、こちら までどうぞ。