KaiSpace
Login
tech

tarjan算法与联通分量

补充一点《算法竞赛进阶指南》中缺失的部分

有向图强连通分量

1. 用处

  1. 缩点，简化图的处理
  2. 2-SAT问题求解

2. tarjan算法详解

首先可以参考《算法竞赛进阶指南》，这里补充一些没有说清楚的点。

这个算法的思想是，找到每个点是否能够通向其祖先节点，如果可以说明其与祖先节点行成grouping。如果算法结束后id = low，说明它并不与任何祖先节点行程grouping，但是可以与其子节点行程grouping。

这个算法最后并不是low相等为一个grouping，而是在返回时进行判断id == low，并且出栈到当前节点。换句话说，当前节点上面的所有点都属于以这个节点为最小id的grouping中。

书中将节点划为三种状态：未访问，访问了但是能够用于更新，访问但是不能用于更新，我们按照这个定义来解释这个算法的正确性：

如果某个之前访问过的sibling节点仍然能用于更新，说明两者的共同祖先在sibling的环中，如果能够连向这个节点，说明当前节点可以通向其祖先节点，所以它也在环中。如果某个节点A不能再用于更新，说明它自己或其祖先节点不能连向更上面的点，而由于搜索到了当前点时，其祖先节点都不会是不能更新状态，所以其祖先节点不可能与节点A形成环。于是这个算法正确的充要条件得到验证。

其次，书中在用栈中元素更新时写low[x] = min(low[x], dfn[y])，其实low[x] = min(low[x], low[y])也是可以的，我们所需要保证的只是更新后low[x] != dfn[x]。

3. 代码实现

#include<bits/stdc++.h>
using namespace std;
int node[10005]; //store the first edge
stack<int> visiting;//使用stack和canvisit实现O(1)判断是否可用于更新以及出栈
priority_queue<int, vector<int>, greater<int> > scc[10005];
bool sccused[10005];
int scccnt;
int belong[10005];
struct mark{
	int id;
	int low;
	int canvisit;
	int visited;
} mark[10005];
struct edge {
	int start;
	int end;
	int nxt;
} e[100005];
void add_edge(int start,int end) { //adjacency list
	static int cnt = 1;
	if (node[start] == 0) {
		edge tmp = {.start = start, .end = end, .nxt = 0};
		e[cnt] = tmp;
		node[start] = cnt;
	} else {
		edge tmp = {.start = start, .end = end, .nxt = node[start]};
		e[cnt] = tmp;
		node[start] = cnt;
	}
	cnt++;
}

int dfscnt;
void dfs(int now) {
	mark[now].id = dfscnt;
	mark[now].low = dfscnt;
	dfscnt++; 
	mark[now].visited = 1;
	mark[now].canvisit = 1;
	visiting.push(now);
	int nxt = node[now];
	while(nxt != 0) {
		int nextNode = e[nxt].end;
		if (mark[nextNode].canvisit) { //visited but can visit, get min
			mark[now].low = min(mark[now].low, mark[nextNode].low);	
		} else if (!mark[nextNode].visited) { //not visited, visit
			dfs(nextNode);
			mark[now].low = min(mark[now].low, mark[nextNode].low);
		}
		nxt = e[nxt].nxt;
	}
	if (mark[now].id == mark[now].low) { //not in groupings with previous nodes
		while(!visiting.empty()) {
			scc[scccnt].push(visiting.top());
			belong[visiting.top()] = scccnt;
			mark[visiting.top()].canvisit = 0;
			if (visiting.top() == now) {
				visiting.pop();
				break;
			}
			visiting.pop();
		}
		scccnt++;
	}
	return ;
}

int main() {
	int n, m, start, end;
	scanf("%d %d", &n, &m);
	for (int i = 1; i <= m; i++) {
		scanf("%d %d", &start, &end);
		add_edge(start, end);
	}
	dfscnt = 1;
	for (int i = 1; i <= n; i++) {
		if (mark[i].visited == 0) {
			dfs(i);
		}
	}
	printf("%d\n", scccnt);
	for (int i = 1; i <= n; i++) {
		int tmp = belong[i];
		if(!sccused[tmp]) {
			while(!scc[tmp].empty()) {
				printf("%d ", scc[tmp].top());
				scc[tmp].pop();
			}
			printf("\n");
			sccused[tmp] = 1;
		}
	}
	return 0;
}

4. 2-SAT问题在CS中的用途（ChatGPT生成）

2-SAT问题：通过找到scc，在O(V+E)时间判断多个命题是否一定不可能同时成立。按照蓝书上所说建2N个点，Vi和Vi′V_i和V_i'。如果ViV_i存在逻辑路径通向Vi′V_i'，同时Vi′V_i'也有逻辑路径通向ViV_i，则证明无论ViV_i为0还是1都不可能满足命题。这个路径问题能够简化为ViV_i和Vi′V_i'是否在一个强连通分量内。

约束满足问题
2-SAT 是布尔可满足性问题（SAT）的一个特例，其约束条件仅包含两个文字的子句。由于 2-SAT 可以在多项式时间内求解，因此在需要验证一系列逻辑约束是否可以同时满足的场景中非常有用。例如，在配置管理、资源分配和任务调度等问题中，经常需要判断一系列条件是否能同时成立。

编译器与程序分析
在编译器优化和静态代码分析中，经常需要对程序中的各种约束（例如类型检查、变量依赖关系、数据流分析）进行判断。2-SAT 问题模型可以用来描述某些特定的约束条件，并通过高效的算法快速验证约束是否一致，从而帮助优化和错误检测。

电路设计与验证
在数字电路设计中，布尔逻辑的约束条件是核心问题。2-SAT 能够有效地解决某些简单的逻辑约束问题，使得设计人员能够验证电路在给定约束下的正确性，确保电路设计无冲突。

模型检测与系统验证
在模型检测领域，2-SAT 常用于验证系统状态转换的可达性及系统约束的满足情况。这对于确保系统没有死锁、无限循环或其他潜在缺陷具有重要意义。

图算法中的应用
2-SAT 问题的求解通常依赖于强连通分量（SCC）分解算法，这种方法不仅在理论上提供了多项式时间的解决方案，也为图的其他应用（例如依赖分析、网络流等）提供了启示和工具。

无向图点双连通分量

(to be continued)

无向图边双连通分量

(to be continued)

Comments

No comments yet.