【集训整理】2-SAT问题 模板题

---

题面：

m 个约束条件，第 j 个约束条件有四个整数 u,x,v,y，表示 $a_u=x$与 $a_v=y$两者至少有一个成立。请判断是否至少存在一组 a 的值满足上述条件。

2-SAT是2-Satisfiability的意思，给一堆布尔变量，每个只有两种选择（1或0），要求满足方程组。

2-SAT的解题方法和差分约束一样是转化为图，然后对图进行操作。

要转化成图，可以把原式化成蕴含式（或者理解成如果...则一定...），给a、非a，b、非b分别建一个点，然后根据蕴含式的箭头连接边，这样就可以转换成图了。

这里的边（箭头）表示逻辑蕴含关系，因此同一个强连同分量内的变量值一定是同时成立的。也就是说，如果出现了如非a和a在同一个强连通分量里，那么就出现了矛盾，这个方程组是无解的。

这样就把方程组转化成了图论的找强连通分量的问题。

转换的方法：

原式	建图
$eg a\vee b$	$a\rightarrow b\wedge\neg b\rightarrow\neg a$
$a \vee b$	$eg a\rightarrow b\wedge\neg b\rightarrow a$
$eg a\vee\neg b\space \space$	$a\rightarrow\neg b\wedge b\rightarrow\neg a$

然后用tarjan找强连通分量即可。

#include<cstdio>
#include<vector>
#include<stack>
using namespace std;
int n, m;
#define maxn 2000005
vector<int> vec[maxn];
int low[maxn], dfn[maxn],color[maxn], cnt = 0,cnt2 = 0;
bool vis[maxn];
stack<int> sta;

void tarjan(int u) {
	low[u] = dfn[u] = ++cnt;
	sta.push(u);
	vis[u] = true;
	for (int v : vec[u]) {
		if (!dfn[v]) {
			tarjan(v);
			low[u] = min(low[u], low[v]);
		}
		else if (vis[v]) {
			low[u] = min(low[u], dfn[v]);
		}
	}
	if (low[u] == dfn[u]) {
		cnt2++;
		while (sta.top() != u) {
			color[sta.top()] = cnt2;
			vis[sta.top()] = 0;
			sta.pop();
		}
		color[sta.top()] = cnt2;
		vis[sta.top()] = 0;
		sta.pop();
	}

}

int main() {
	scanf("%d %d", &n, &m);
	for (int i = 1; i <= m; i++) {
		int u, x, v, y;
		scanf("%d %d %d %d", &u, &x, &v, &y);
		//建图
		if (!x && !y) {
			vec[u + n].push_back(v);
			vec[v + n].push_back(u);
		} else
		if (!x && y) {
			vec[v].push_back(u);
			vec[u + n].push_back(v+n);
		} else
		if (x && !y) {
			vec[v + n].push_back(u+n);
			vec[u].push_back(v);
		} else
		if (x && y) {
			vec[u].push_back(v + n);
			vec[v].push_back(u + n);
		}
	}

	for (int i = 1; i <= n * 2; i++) {
		if (!dfn[i]) tarjan(i);
	}

	for (int i = 1; i <= n; i++) {
		if (color[i] == color[i + n]) {
			printf("NO");
			return 0;
		}
	}

	printf("YES");

}