Dijkstra算法正确性证明

问题：求图中点1到其他各点的最短距离

算法描述：

设初始时图的所有点的集合U

1. 把起点s放入初始集合Set中

   U=U-{s}

   Set=Set+{s}

2. 找s经过集合Set中的点，能达到的距离最短的点k(k\(\in\)U)，将k并入Set

   言外之意k的前一个点必然属于Set

   U=U-{k}

   Set=Set+{k}

   由于每次引入的只有一个点k，所以只需要基于k对s到达所有点的距离进行更新，之前的点无需考虑

3. repet step2

   until U == Set

算法正确性证明：

1. 变量的命名：

Set={1,2,,,,,,x}

记录已求出最短路径的顶点

dist[u]

从start点开始，经过Set中的点，到u点(u\(\in\)U)的最短距离

short[u]

从start开始到u的全局最短路径(路径中可能有部分点\(\notin\)Set)

可知 \(short[u]\leq dist[u]\)

U

所有点除去Set中的点组成的集合

2. 证明过程：(贪心正确性的证明)

需要证明的命题：

算法进行到第k步时，Set中的任意一个节点Set_i的dist[Set_i]等于全局最短路径short[Set_i]

(第n步时，dist[n]=short[n]，此时找到点1到所有点的最短距离)

归纳基础：

k=1，Set={start_point} => dist[start_point] == short[start_point] ==0，命题正确

归纳假设：

假设第k步成立，现在来证明第k+1步成立

第k步成立的作用在于s到Set中的所有节点(设某节点为k)有dist[k]=short[k]

所以对于引入的第k+1个点v，s->v序列中Set中的点一定是连续的(如下图。因为s->v中的Set的最后一个点u之前的所有点必然都属于Set)

设k+1步选择了顶点v(v是s经过Set所能到达的U中距离最近的点)

则顶点v必然与Set中的u点直接相连， 也就是说上图中非Set中的点集为空集

证明如下：

假设蓝色部分“非Set中的点”所组成的集合不为空，也就是s到v的最短路径是先有一部分Set中的点，再由一部分U中的点组成，那么

short[v]：s->...->u->...->y->...->v

如下图

　　

　　　

因为之前论证过s->u(u代表Set集合中的最后一个点)过程中所有的点均属于Set，所以有：

1. s->...->u1->v
2. s->...->u2->y->v

易知length(s->...->u1->v)\(\leq\)length(s->...->u2->y)

v是s经由Set所能达到的距离最小点

又length(y->v)$\geq$0

所以不存在这样的y，s到v的最短路径上v的前一个节点必然为Set中的点

从而也就论证了迪杰斯特拉算法的正确性