使用存在量词的高效联合查找？

Question

有没有经典的算法来解决下面的问题。假设不带存在量词的联合查找算法具有以下输入：

x1 = y1 /\ .. /\ xn = yn

然后，它将构建一些数据结构u，以便我可以检查u.root(x)==u.root(y)，以确定x和y是否在同一子图中。

输入可以通过以下语法来表征：

Input :== Var = Var | Input /\ Input

假设现在我们也允许存在量词：

Input :== Var = Var | Input /\ Input | exists Var Input

什么样的联合查找算法可以处理这样的输入。我仍然假设算法建立了一些数据结构u，我可以通过u.root(x)==u.root(y)检查x和y是否在同一个子图中。

此外，当与绑定变量一起使用时，u.root(x)应该抛出异常。这些变量都应该被删除，并且不再是数据结构的一部分。意味着子图应该相应地减少，而不会改变结果的有效性。

再见

Answer 1

这是一个算法的草图。它将遍历AST，并提供一个特殊的联合查找算法。首先是遍历：

 traverse((X = Y)) :- add_conn(X, Y).
 traverse(exists(X,I)) :- push_var(X), traverse(I), pop_var_remove_conn(X).
 traverse((A /\ B)) :- traverse(A), traverse(B).

特殊的联合查找算法使用列表。该列表定义了节点的权重，列表头部的权重为0，第二个元素的权重为1，依此类推。add_conn(X，Y)首先计算X‘=根(X)和Y’=根(Y)。X‘和Y’的权重越小，则连接到权重越大的那个。

push_var(X)将X加到列表的前面。使其成为权重较小的节点。pop_var_remove_conn(X)再次从列表中删除X，并删除从X到其他节点的可能已建立的连接。