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

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) 在使用时应该抛出异常带有绑定(bind)变量。这些变量都应该是被淘汰，不再是数据结构的一部分。方法子图应该相应地减少，没有改变结果的有效性。

再见

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'=root(X) 和 Y'=root(Y)。这权重较小的 X' 和 Y' 与权重较大的相关联。

push_var(X) 将 X 添加到列表的前面。使它的权重更小节点。 pop_var_remove_conn(X) 再次从列表中删除 X，并删除一个也可能建立从 X 到其他某个节点的连接。