括号定理
概述
括号定理(Parenthesis Theorem):在有向图(或无向图)的深度优先搜索中,任意两个顶点 和 的发现时间与完成时间构成的时间戳区间 和 要么完全不相交,要么一个完全包含另一个。这一性质与括号的嵌套结构完全对应。
定理陈述
形式化陈述
定理(CLRS 定理22.7):在对(有向或无向)图 的任何深度优先搜索中,对于任意两个顶点 和 ,以下三种情况恰好有一种成立:
- 区间不相交: 与 完全不相交,且 和 之间没有祖先-后代关系
- 的区间包含 的区间:, 是 的真祖先(proper ancestor)
- 的区间包含 的区间:, 是 的真祖先(proper ancestor)
此外,DFS 边分类与时间戳的关系为:
- 是树边或前向边
- 是后向边
- 是横边
证明概要
证明思路
证明分为两部分:先证明括号定理本身(区间嵌套性质),再推导边分类与时间戳的对应关系。
第一部分:括号定理的证明
对 DFS-VISIT 的调用次数进行归纳。
归纳基础:第一次调用 DFS-VISIT 时,只有一个顶点 ,产生唯一的时间戳区间 。只有一个区间,性质平凡成立。
归纳步骤:设在调用 DFS-VISIT() 之前,所有已完成的时间戳区间满足括号性质。考虑 DFS-VISIT() 的执行:
- 被设置, 变为 GRAY(“左括号”)
- 对于 的每个 WHITE 邻居 ,递归调用 DFS-VISIT():
- 由归纳假设, 及其后代的时间戳区间正确嵌套在 中
- 由于 ( 在 之后被发现)且 ( 在 之前完成),区间 完全包含在 中
- 的多个 WHITE 邻居产生的时间戳区间互不相交(因为它们按顺序被发现和完成)
- 被设置, 变为 BLACK(“右括号”)
新产生的时间戳区间与之前已完成的时间戳区间也不相交(因为之前完成的顶点在 被发现之前就已经完成)。综上,括号性质始终成立。
第二部分:边分类与时间戳关系的证明
树边: 在 的递归搜索过程中被发现( 为 WHITE)。 的 DFS-VISIT 在 的 DFS-VISIT 完成之前结束,故 。
前向边: 是 的后代但不是通过树边到达( 为 BLACK 且 )。由括号定理, 的时间戳区间完全包含在 的区间内,故 (与树边的时间戳条件相同)。
后向边: 是 的祖先( 为 GRAY)。由括号定理, 的时间戳区间完全包含在 的区间内,故 。
横边: 和 无祖先-后代关系( 为 BLACK 且 )。由括号定理,两个区间不相交,且 在 之前被发现和完成,故 。
参考文献:
- CLRS 第4版,第20.3节 “Depth-first search”,定理22.7
- Tarjan, R.E., “Depth-first search and linear graph algorithms”, SIAM J. Comput., 1(2):146-160, 1972
关键推论
- 祖先-后代的等价判定: 是 的祖先 。时间戳完全决定了 DFS 森林中的祖先-后代关系。
- 白色路径定理(定理22.9): 是 的后代 在时刻 存在从 到 的全白色路径。括号定理是其证明的关键工具。
- 无向图只有两类边:在无向图 DFS 中,每条边要么是树边,要么是后向边。前向边和横边不存在(因为无向边的双向检查性质)。
- 后向边等价于有向回路:有向图中存在后向边当且仅当图中存在有向回路,这是 DAG 判定的理论基础。
应用场景
在算法导论中的具体应用:
- DFS 边分类(Ch20):括号定理为 DFS 的四种边分类(树边、后向边、前向边、横边)提供了基于时间戳的判定准则,无需在 DFS 执行过程中实时记录边类型。
- 有向回路检测:通过检查是否存在后向边(),在 时间内判定有向图是否为 DAG。
- 强连通分量(Ch20.5):Kosaraju 算法和 Tarjan SCC 算法都依赖括号定理所揭示的 DFS 时间戳结构来识别强连通分量。
- 拓扑排序(Ch20.4):括号定理保证了”完成时间晚的顶点排在前面”的正确性,是拓扑排序算法的理论基础。