SCC-Tarjan算法正确性证明

July 1, 2014 at 11:44 pm

注:这篇文章由于存在不少错误而暂时(可能永久)地被废弃,相关的内容请转至图论算法漫谈之连通性(二):tarjan求强连通分量 Tarjan算法应该是求有向图强连通分量的最常用的算法,而且本身也非常的高效。网上关于Tarjan算法的介绍、模板都非常多,这里炒冷饭的目的是打算证明一下Tarjan算法的正确性,在网上找了好久,都没能找到一个我这种水平也能看得懂的证明,所以打算自己写一个。证明的主要参考来自Tarjan大神的论文。 强连通分量的概念 设G是一个有向图。如果对于G中的每个点v, w,都存在一条v到w的路径和w到v的路径(下文对于v到w的边表示为v=>w,v到w的路径表示为v==>w),那么称G是强连通的(strongly connected)。 对于G中的点v, w,如果存在v==>w和w==>v,那么称v和w是强连通的。为了引出强连通分量的概念,这里证明在G的点上的强连通关系是个等价关系。其中对称性、自反性是显然的,简单说明一下传递性。如果v和w强连通,而w和y强连通,v==>w,w==>y,v==>y,反之亦然,所以这显然是个等价关系。由于点的强连通性是一个等价关系,图G中的点就被划分成若干个等价类,而每个等价类中的点和它们在原G中的边显然构成一个强连通子图。于是图G就分解成若干个强连通子图(以及可能存在的连接这些子图的边),每一个子图就成为G的一个强连通分量(strongly connected component, SCC)。 DFS搜索树 Tarjan算法主要使用了DFS,并充分利用了DFS过程的特性。为了阐述的方便,下面以一个实际的图为例,介绍在DFS搜索中的一些概念。 上图给出了一个有向图,包括它的的所有顶点和所有边(包括所有虚线边)。 图中的编号对应了DFS遍历的顺序,在tarjan算法中,每个顶点的遍历序号通常记为DFN(v),也称为时间戳(从1开始)。 图中所有蓝色的边及相应顶点构成了一次DFS的搜索树,这些蓝色的边是树上的边,我们记树上的边(v, w)为       […]