三路不相交问题算法正确性证明及循环不变式探究

问题背景 #

我们需要实现一个算法，判断三个非空整数集合（分别用数组A、B、C表示）的交集是否为空。以下是实现的Python代码：

def disjoint(A, B, C):
    """Solves (?) three-way disjointness problem in n*log(n) time.
    """

    A = sorted(A[:])
    B = sorted(B[:])
    C = sorted(C[:])

    i = j = k = 0
    while i < len(A) and j < len(B) and k < len(C) and (A[i] != B[j] or B[j] != C[k]):
        if A[i] <= B[j] and A[i] <= C[k]:
            i += 1
        elif B[j] <= A[i] and B[j] <= C[k]:
            j += 1
        else:
            k += 1

    if i < len(A) and j < len(B) and k < len(C):
        return False
    else:
        return True

该算法通过了测试，但需要对其正确性进行半形式化证明，核心问题包括：

• 如何证明算法的正确性？
• 适合该算法的循环不变式是什么？
• 若算法存在错误，请给出反例。

算法正确性证明 #

1. 循环不变式定义 #

在每次循环迭代开始前，以下命题成立：

不存在任何元素x，使得x同时属于A[0..i-1]、B[0..j-1]、C[0..k-1]；并且如果三个集合的交集非空，那么交集元素一定存在于A[i..len(A)-1]、B[j..len(B)-1]、C[k..len(C)-1]的共同部分中。

2. 初始化验证（i=j=k=0时） #

此时A[0..i-1]、B[0..j-1]、C[0..k-1]都是空集，显然不存在共同元素；而三个集合的所有元素都在剩余的子数组中，完全符合不变式的两个条件。

3. 循环保持验证 #

假设在某次迭代开始前，循环不变式成立。我们需要证明迭代结束后不变式仍然成立：

循环的执行条件是i < len(A)、j < len(B)、k < len(C)且A[i] != B[j] 或 B[j] != C[k]，即当前三个指针指向的元素不全相等。

根据循环内的分支逻辑：

• 若A[i]是三个元素中的最小值：由于B、C已排序，后续元素都≥当前B[j]、C[k]，而A[i]≤这两个值且三者不全相等，因此A[i]不可能在B[j..]和C[k..]中找到相等元素，即A[i]不可能属于三个集合的交集。将i加1后，剩余的候选交集元素仍在A[i..]、B[j..]、C[k..]中，不变式保持。
• 若B[j]是三个元素中的最小值：同理，B[j]不可能在A[i..]和C[k..]中找到匹配，将j加1后，不变式保持。
• 若C[k]是三个元素中的最小值：同理，C[k]不可能在A[i..]和B[j..]中找到匹配，将k加1后，不变式保持。

因此，每次迭代后循环不变式仍然成立。

4. 终止条件验证 #

循环终止有两种情况：

情况1：i >= len(A) 或 j >= len(B) 或 k >= len(C)

根据循环不变式，此时不存在同时属于三个集合的元素，算法返回True（交集为空），结果正确。

情况2：A[i] == B[j] == C[k]

此时找到了三个集合的共同元素，算法返回False（交集非空），结果正确。

结论 #

该算法是正确的，上述循环不变式可以完整支撑其正确性的半形式化证明。

内容的提问来源于stack exchange，提问作者user6419965