为了方便理解，咱们可以先看一组实例。
今天huge要买水果
lbtl说：
1.我不吃梨(\(\neg a\))
2.我吃苹果（b）
3.我吃草莓（c）
lxyt说：
1.我吃梨（a）
2.我吃苹果（b）
3.我不吃草莓（\(\neg c\)）
CTH说：
1.我不吃梨（\(\neg a\)）
2.我不吃苹果（\(\neg b\)）
3.我不吃草莓（\(\neg c\)）
（huge:不吃，滚）
我们不妨根据逻辑运算符给他们设计一下状态
lbtl\((\neg a \vee b \vee c)\)
lxyt\((a \vee b \vee \neg c)\)
CTH\((\neg a \vee \neg b \vee \neg c )\)
而他们同时满足则为
\((\neg a \vee b \vee c) \wedge (a \vee b \vee \neg c) \wedge (\neg a \vee \neg b \vee \neg c )\)
那么很好，我们就需要一个算法来处理这个，2-SAT闪亮登场，那既然它都叫“2”-SAT了，那自然是只有两个限定条件，于是我们把想不想吃草莓这一状态删掉，这样就转化为了了2——SAT类型。
那我们如何去解决2—SAT问题呢？
我们可以想到差分约束，通过建图，在图上进行操作来解决。于是我们就可以用强联通分量来搞它。
那差分约束最困难的地方是连边，2-SAT也是如此。先看一道例题
那我们正常想的连边
点击查看代码
a=read();x=read(); //第a个数为x或第b个数为y
b=read();y=read();
if(x==0&&y==0) //"如果第a个数为0或第b个数为0"至少满足其一
{
add(a+n,b); //a=1则b=0
add(b+n,a); //b=1则a=0
}
if(x==0&&y==1) //"如果第a个数为0或第b个数为1"至少满足其一
{
add(a+n,b+n); //a=1则b=1
add(b,a); //b=0则a=0
}
if(x==1&&y==0) //"如果第a个数为1或第b个数为0"至少满足其一
{
add(a,b); //a=0则b=0
add(b+n,a+n); //b=1则a=1
}
if(x==1&&y==1) //"如果第a个数为1或第b个数为1"至少满足其一
{
add(a,b+n); //a=0则b=1
add(b,a+n); //b=0则a=1
}
至于为什么
看看佬的blog
但我们可以利用二进制来简化
点击查看代码
for(int i=1;i<=m;i++)
{
int a=read(),va=read(),b=read(),vb=read();
add(a+n*(va&1),b+n*(vb^1));
add(b+n*(vb&1),a+n*(va^1));
}
连完边之后，我们就可以跑tarjan了，但要注意tarjan跑出的是拓扑逆序，最后判断的时候要反过来。
点击查看代码
#include<bits/stdc++.h>
using namespace std;
const int N=3e6;
int n,m;
int read()
{
int f=1,s=0;char ch=getchar();
while(ch<'0'||ch>'9'){if(ch=='-')f=-1;ch=getchar();}
while(ch>='0'&&ch<='9'){s=(s<<3)+(s<<1)+(ch^48);ch=getchar();}
return s*f;
}
int h[N],to[N],nxt[N],tot;
void add(int x,int y)
{
to[++tot]=y;
nxt[tot]=h[x];
h[x]=tot;
}
int low[N],dfn[N],dfncnt;
int s[N],in_stack[N],tp;
int scc,sc[N];
void tarjan(int u)
{
low[u]=dfn[u]=++dfncnt;
in_stack[u]=1;
s[++tp]=u;
for(int i=h[u];i;i=nxt[i])
{
int v=to[i];
if(!dfn[v])
{
tarjan(v);
low[u]=min(low[u],low[v]);
}
else if(in_stack[v])
{
low[u]=min(low[u],dfn[v]);
}
}
if(dfn[u]==low[u])
{
scc++;
while(s[tp]!=u)
{
sc[s[tp]]=scc;
in_stack[s[tp]]=0;
tp--;
}
sc[s[tp]]=scc;
in_stack[s[tp]]=0;
tp--;
}
}
int main()
{
n=read(),m=read();
for(int i=1;i<=m;i++)
{
int a=read(),va=read(),b=read(),vb=read();
add(a+n*(va&1),b+n*(vb^1));
add(b+n*(vb&1),a+n*(va^1));
}
for(int i=1;i<=n*2;i++) if(!dfn[i]) tarjan(i);
for(int i=1;i<=n;i++)
{
if(sc[i]==sc[i+n])
{
puts("IMPOSSIBLE");
exit(0);
}
}
puts("POSSIBLE");
for(int i=1;i<=n;i++)
{
printf("%d ",sc[i]<sc[i+n]);
}
}