次の問題を解決するための古典的なアルゴリズムはありますか。存在量指定子を使用しない和集合検索アルゴリズムに次の入力があるとします。
x1 = y1 /\ .. /\ xn = yn
次に、u.root(x)==u.root(y) をチェックして、x と y が同じサブグラフにあるかどうかを判断できるように、データ構造 u を構築します。
入力は、次の文法によって特徴付けることができます。
Input :== Var = Var | Input /\ Input
ここで、存在量指定子も許可するとします。
Input :== Var = Var | Input /\ Input | exists Var Input
そのような入力を処理できるユニオン検索アルゴリズムはどれですか。x と y が同じサブグラフにあるかどうかを u.root(x)==u.root(y) 経由でチェックできるアルゴリズムが何らかのデータ構造 u を構築するとまだ仮定しています。
さらに、u.root(x) は、バインドされた変数で使用すると例外をスローする必要があります。これらの変数はすべて削除され、データ構造の一部ではなくなりました。結果の有効性を変更することなく、サブグラフがそれに応じて削減されるべきであることを意味します。
さよなら