更多「图论」相关证明文章见如下帖子:
图论相关证明文章列表
【目录】
Dijkstra算法(狄杰斯特拉算法):
一种基于广度优先搜索和贪婪思想的求解 无负边有向赋权图单源最短路径 的算法。
算法将所有顶点区分为「到源点 的最短距离」(以后简称「距离」) 已确定 和 未确定 的顶点。算法开始前所有顶点的距离均未确定(一般置为),初始时置 的距离为 0。以一个while循环查询当前 是否有距离未确定 的顶点,若有则将其中距离最小者 选为 当前顶点,并使其距离已知。然后以BFS的方式松弛 的邻接顶点 并更新 的前驱为 。当不再有未确定距离的顶点时算法结束,此时每一个顶点的距离均最小。通过递归寻找节点的前驱可以得到 到该顶点的具体的最短路径。
松弛操作 是最短路径算法的关键,在确定当前顶点 (最新成为已确定距离的顶点) 后立即操作,目的是更新 的邻接顶点 的距离和其前驱。如下图, 经过若干个顶点到 和 , 和 邻接 。假设此时 ,,。
先于 成为当前顶点,由于 ,故 松弛 ,并将 的前驱置为 ,。
成为当前顶点时,由于 ,故 松弛 ,并将 的前驱置为 ,。

一个直观的观察是,来自 入边的松弛,使得 不断更新至所有可能的路径距离的最小值。以下严格证明该算法正确性。
利用数学归纳法(结合反证法)证明。
本证明参考了这个帖子。
起始验证。对于命题 ,当 时命题 成立。
假设命题成立。假设命题 在 时成立。
递推证明。根据2的假设,若能证明 时命题 成立,则命题得证。
例如,有命题 ,按照数学归纳法证明如下:
起始验证。当 等于 时,,命题成立。
假设命题成立。假设命题等于 时成立,。
递推证明。根据2的假设,如果能证明 时命题正确,则命题 成立。
证明:在2所示式子左右两边加上 ,得到
等号右边可以写成 ,显然该形式就是将 代入原命题 的形式,证毕。
命题 :Dijkstra算法第 次进入while时,会将第 个顶点加入距离已确定顶点集合 中,此时对于顶点 共 个),总有 。
※ 表示由Dijkstra算法得到的最短距离估计,对于源点 ,在程序开始时赋予 ,对于其他顶点,由松弛操作得到。 表示实际的顶点 到源点的最短距离。
起始验证。当 等于 时, 集合中只有源点 自身, (程序开始时赋值得到),且知 ,故 时命题正确。
假设命题成立。假设命题 在 等于 时, 成立,即算法经过 次while,得到具有 个顶点的集合 ,对于顶点 (共 个),总有 。
递推证明。根据 2 的假设,如果能证明第 个顶点 被放入集合 时有 ,则命题 成立。
更详细地, 时,在点集 中根据算法规则找到距离最短的顶点 ,将该顶点将作为第 个顶点放入A中,放入后 ,如果能证明 ,使得 成立,则对于顶点 (共 个),有 。
以反证法证明之。
(1)
※ 是实际的 到源点的最短距离, 不成立时只能是 。算法保证了从 到 的过程一定是一条由图中的有向边构成的 连续路径,只要是连续路径,无论有多少条这样的路径,一定有一条最短路径,其长度记作 。并使得其他路径长度必大于等于
(2)
这是显然的,因为 是 的一部分,当 时取到等号。

3.3 🤔 在 之前被选中进入 集内时,对其邻接顶点 执行过 松弛操作,该操作会比较 是否小于 ,若小于则以 更新 的值,所以如果更新了,更新之后有 ,如果没更新,说明 。假设之后 还会被 的其他前驱顶点更新 值 (当该前驱顶点进入 集时),那 只会变得更小,所以一定有:
(3)
比较式 (2) 和式 (3) 中的 和 ,因为 (由步骤2的 假设给出,顶点 是 假设的 个顶点之一),而 只是若干从 到 的路径之一,因此必有 ,当 恰是 到 的最短路径时取到等号。所以根据式 (2) 和式 (3) 有:
,即
(4)
3.4 🤔 顶点 与 均在 集中,根据算法规则, 作为第 个定点被放入 集中时,其在 集中相比于 集中的其他顶点(自然也包括 ),到源点 的距离最小,显然有:
(5)
结合式 (1),式 (4),式 (5)得到:
(6) ,即
至此,由3.1的假设 「 不成立」导出了 矛盾,所以 是成立的,Dijkstra算法正确性得证。