验证带提前终止检查的树染色后最小距离DFS算法正确性

问题背景 #

给定一棵初始所有顶点为白色的树，我们逐个将顶点染为黑色，每次染色后需要找出当前所有黑色顶点对之间的最小距离（距离为路径上的边数）。

我的实现思路 #

我使用min_dist[]数组（0索引）存储每个顶点u到最近黑色顶点的距离，每次染色后通过深度优先搜索（DFS）求解。设G为树结构，c[]是按染色顺序排列的顶点数组，具体算法实现如下：

SOLVE主函数 #

SOLVE(G, c)
1. ans = +(infinity)
2. for (i = 0 to (|G.V| - 1))
3.     min_dist[i] = +(infinity)
4. for (i = 0 to (|G.V| - 1))
5.     min_dist[c[i]] = 0
6.     DFS(G, ans, min_dist, c[i], -1)
7.     print ans

原DFS函数 #

DFS(G, ans, min_dist, v, parent)
1. for (each vertex child in G.Adj[v])
2.     if (child == parent)
3.         continue
4.     if (min_dist[child] > min_dist[v] + 1)
5.         min_dist[child] = min_dist[v] + 1
6.         DFS(G, ans, min_dist, child, v);
7.     else if (ans > min_dist[child] + min_dist[v] + 1)
8.         ans = (min_dist[child] + min_dist[v] + 1)

官方优化版本 #

官方解法在DFS函数开头增加了提前终止检查，修改后的DFS如下：

DFS(G, ans, min_dist, v, parent)
1. if (min_dist[v] >= ans)
2.     return
3. for (each vertex child in G.Adj[v])
   ... 

我已经用多个测试示例验证了这个修改版本的正确性，但需要从理论上证明这个带提前终止检查的DFS算法是正确的。

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