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

}
```


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://blog.mcyou.cc/suan-fa-xiang-guan/suan-fa/ji-xun-zheng-li-2sat-wen-ti-mu-ban-ti.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.