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) 在与绑定变量一起使用时应该抛出异常。这些变量都应该被消除，不再是数据结构的一部分。意味着子图应该相应地减少，而不改变结果的有效性。

再见

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 到某个其他节点的连接。