有没有经典的算法可以解决下面的问题。 假设联合查找算法没有存在量词 具有以下输入:
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)变量。这些变量都应该是 被淘汰，不再是数据结构的一部分。方法 子图应该相应地减少，没有 改变结果的有效性。
再见
最佳答案
这是一个算法的草图。它将遍历 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 到其他某个节点的连接。
关于algorithm - 使用存在量词的高效联合查找？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/28148184/