SAT(Satisfiability)问题：
有n个$bool$变量，m个需要满足的条件，形如“xi为true || xj为false || xk为 false…”。
给每个变量赋值，使得所有条件得到满足。
SAT问题已被证明为NP完全，只能暴力枚举求解。
特别地，如果每个条件中约定的变量只有2个，那么就可以用tarjan强连通分量求解，即2-SAT问题。
感性理解：
假设有一些“若x，则y”的条件，将$x$-> $y$连边。
建图后，使用tarjan缩点，若发现x和非x在同一连通块内，则一定无解。
那么，对于“x||y”的条件，可以把它转变为“若!x，则y”&&“若!y，则x”。
将以上两个条件连边。一共有n个节点，!i的编号可以表示为i+n。
tarjan缩点后，检查点1~n是否有$col[i] = col[!i]$，若有则无解。
tarjan得出连通块的编号col[]恰好是拓扑序的逆序。拓扑序在后边的，对其他的节点影响小。
所以输出方案时，$col[i] < col[!i]$则选i，否则选-i。
代码如下
#include<cstdio> #include<iostream> #include<cmath> #include<cstring> #define MogeKo qwq using namespace std; const int maxn = 2e6+10; int n,m,x,y,a,b,cnt,num,tot,top; int dfn[maxn],low[maxn],sta[maxn],col[maxn]; bool insta[maxn]; int head[maxn],to[maxn],nxt[maxn]; void add(int x,int y) { to[++cnt] = y; nxt[cnt] = head[x]; head[x] = cnt; } void tarjan(int u) { dfn[u] = low[u] = ++tot; insta[u] = true; sta[++top] = u; for(int i = head[u]; i; i = nxt[i]) { int v = to[i]; if(!dfn[v]) { tarjan(v); low[u] = min(low[u],low[v]); } else if(insta[v]) low[u] = min(low[u],dfn[v]); } if(dfn[u] == low[u]) { col[u] = ++num; while(sta[top] != u) { int v = sta[top--]; col[v] = col[u]; insta[v] = false; } top--; insta[u] = false; } } int main() { scanf("%d%d",&n,&m); for(int i = 1; i <= m; i++) { scanf("%d%d%d%d",&x,&a,&y,&b); add(x+(!a)*n, y+b*n); add(y+(!b)*n, x+a*n); } for(int i = 1; i <= 2*n; i++) if(!dfn[i]) tarjan(i); for(int i = 1; i <= n; i++) if(col[i] == col[i+n]) { printf("IMPOSSIBLE "); return 0; } printf("POSSIBLE "); for(int i = 1; i <= n; i++){ if(col[i] < col[i+n]) printf("0 "); else printf("1 "); } return 0; }