Dijkstra正确性定理
概述
Dijkstra正确性定理:Dijkstra 算法在边权非负的加权图中,能正确计算从源点到所有其他顶点的单源最短路径。该定理通过数学归纳法(或等价地,通过循环不变量)严格证明了贪心选择——每次取出距离最小的未处理顶点——的正确性。
定理陈述
形式化陈述
定理:设 是一个边权非负的加权图(对所有 ,), 为源点。Dijkstra 算法对每个顶点 计算的距离估计值 满足:当 被从优先队列中取出时(即加入集合 时),,其中 是从 到 的最短路径长度。
前置条件:所有边权 。
证明概要
证明思路
使用数学归纳法(等价于循环不变量方法)证明。核心是建立关于集合 (已确定最短距离的顶点集)的归纳不变量。
循环不变量:在每次迭代开始时( 为当前已处理顶点集),以下性质成立:
- (I1) 对所有 ,(已处理顶点的距离是正确的)
- (I2) 对所有 ,(未处理顶点的距离是从 经 中顶点到达的最短路径长度)
步骤 1:初始化——验证基础步
初始时 ,,其余 。
- (I1): 为空,条件平凡成立
- (I2): 为空,不存在从 经 到达 的路径, 正确
步骤 2:保持——归纳步
假设不变量在某次迭代开始时成立。设 是 中 值最小的顶点,将 加入 。
证明 (即 (I1) 对 成立):
反证法。假设 ,即存在从 到 的更短路径。考虑这条最短路径 , 从 出发,必定在某个点第一次离开 。设 是 上第一个不在 中的顶点, 是 在 上的前驱()。
则 (由 (I2))。
又因为 是最短路径,。
但 是 中 值最小的顶点,所以 。因此 ,与 矛盾。
证明 (I2) 对更新后的 成立:
加入 后,对每个 ,从 经 到达 的最短路径要么不经过 (长度为 ),要么经过 (长度为 )。松弛操作 正确维护了 (I2)。
步骤 3:终止
当 时,由 (I1),所有顶点的 值都是正确的最短路径长度。
关键引理:上述证明中,边权非负的条件保证了 (不会因为负权边导致绕行后更短)。若存在负权边,该引理不成立,Dijkstra 算法可能给出错误结果。
学术参考:知识库笔记 10.6 最短路径问题 中包含完整的归纳法证明过程。
关键推论
- 单源最短路径的正确性:Dijkstra 算法终止后,对所有 ,
- 负权边的限制:Dijkstra 算法不能处理含负权边的图。对于含负权边(但无负权回路)的图,应使用 Bellman-Ford 算法
- 优先队列实现:使用二叉堆实现的 Dijkstra 算法时间复杂度为
- 与 BFS 的关系:当所有边权为 1 时,Dijkstra 算法退化为 BFS
应用场景
- 算法导论 Ch22:Dijkstra 正确性定理是单源最短路径算法的理论基础
- 网络路由:OSPF 路由协议使用 Dijkstra 算法计算最短路径
- 地图导航:Google Maps 等导航系统的核心算法(通常使用 A* 作为 Dijkstra 的启发式改进)
- 游戏 AI:游戏中的寻路算法(A* 是 Dijkstra 的带启发式版本)
- 社交网络:计算两个人之间的最短关系链
参见
- 贪心算法 — Dijkstra 算法是贪心策略的经典成功案例
- 循环不变量 — 循环不变量三条件与归纳法的对应关系
- 加权图 — 加权图的定义与最短路径问题
- 10.6 最短路径问题 — Dijkstra 算法的详细说明、执行实例与正确性证明