引入：
相信大家都了解过差分约束系统。差分约束系统的大体意思就是给出一些有某种关系的变量，问你是否有某种赋值使得这些关系全部成立
其实(2-SAT)的题目描述和这个很像（虽然解法不一样）
那么(2-SAT)到底是什么呢？
首先，把(2)和(SAT)拆开。(SAT) 是 (Satisfiability) 的缩写，意为可满足性。即一串布尔变量，每个变量只能为真或假。要求对这些变量进行赋值，满足布尔方程(摘自(Anguei)的题解)
通俗一点来说，就是有(n)个bool变量(x_1)~(x_n)有(m)个位运算的表达式（只有两个变量），求是否有一种方法使得(m)个表达式都成立
例题
题目背景
2-SAT 问题 模板
题目描述
有(n)个布尔变量(x_1)~(x_n)，另有(m)个需要满足的条件，每个条件的形式都是"(x_i)为true/false"或"(x_j)为true/false"。比如"(x_1)为真或(x_3)为假"、"(x_7)为假或(x_2)为假"。2-SAT 问题的目标是给每个变量赋值使得所有条件得到满足。
输入格式
第一行两个整数n和m，意义如体面所述。
接下来m行每行4个整数$ i ,a, j, b (，表示")x_i(为a或)x_j(为b"()a,bin {0,1}$)
输出格式
如无解，输出"IMPOSSIBLE"（不带引号）; 否则输出"POSSIBLE"（不带引号),下一行(n)个整数（(x_1)~(x_n)(in {0,1})），表示构造出的解。
如何解决这类问题？
首先，我们发现一个变量取值的真和假是相对独立的，也就是说和他自己没有关系，只和其他变量的真假有关系
那我们不妨为每一个变量建两个节点，一个表示真，一个表示假（我这里用1~n表示假，n+1~2n表示真）
有了点，考虑怎么连边。如果一个变量的真假能够推出另一个变量的真假，就对这两个变量对应的真假连边
比如：(x_1)为真或(x_2)为假，那么(x_1)的假就可以推出(x_2)的真，(x_2)的真就可以推出(x_1)的假
那么就把(x_1)对应的假节点连向(x_2)对应的真节点，把(x_2)对应的真节点连向(x_1)对应的假节点
如何判断有没有解？
考虑无解的情况，肯定是出现了矛盾，也就是一个点的真推出了它自己的假，或者是这个点的假推出了它自己的真。这种情况有什么特征？
发现如果是这样的话，这个点的真和假一定在相同的强连通分量里面
强联通分量？那不就是tarjan吗？
时间复杂度O(n+m)
那么怎么找出满足题意的解？
当(x)所在的强连通分量的拓扑序在( eg x)之后时，直接取(x)为真就行了。tarjan算法在执行的过程中已经为每一个强连通分量标好了拓扑序（不过是和正常的拓扑序相反）
#include<bits/stdc++.h>
using namespace std;
const int N=2000050;
int head[N],ecnt;//1~n存0,n+1~2n存1
struct edge
{
int to,nxt;
}edg[N<<1];
inline void add(int u,int v)
{
edg[++ecnt].to=v;
edg[ecnt].nxt=head[u];
head[u]=ecnt;
}
int n,m;
inline void read()
{
for(int i=1;i<=m;i++)
{
int x,a,y,b;
scanf("%d%d%d%d",&x,&a,&y,&b);//建边
if(a==1&&b==1) add(x,y+n),add(y,x+n);
if(a==0&&b==1) add(x+n,y+n),add(y,x);
if(a==1&&b==0) add(x,y),add(y+n,x+n);
if(a==0&&b==0) add(x+n,y),add(y+n,x);
}
}
//tarjan
int dfn[N],low[N],in[N],s[N],scc[N],top,ind,cnt;
void tarjan(int x)
{
low[x]=dfn[x]=++ind;
s[top++]=x;
in[x]=1;
for(int i=head[x];i;i=edg[i].nxt)
{
int v=edg[i].to;
if(!dfn[v])
{
tarjan(v);
low[x]=min(low[x],low[v]);
}
else if(in[v]) low[x]=min(low[x],dfn[v]);
}
if(dfn[x]==low[x])
{
cnt++;
while(s[top]!=x)
{
top--;
in[s[top]]=0;
scc[s[top]]=cnt;
}
}
}
int main()
{
scanf("%d%d",&n,&m);
read();
for(int i=1;i<=2*n;i++)
{
if(!dfn[i]) tarjan(i);
}
for(int i=1;i<=n;i++) if(scc[i]==scc[i+n]) return cout<<"IMPOSSIBLE",0;
puts("POSSIBLE");
for(int i=1;i<=n;i++) printf("%d ",scc[i]>scc[i+n]);
}