# 【集训整理】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");

}
```