什么是2-sat问题
如给定\(n\)个变量，可以赋值为\(A{_{0} }\)或\(A{_{1} }\)，现给出\(m\)个限制，询问是否存在合法赋值使得\(m\)个询问均成立
很抽象吧
举个例子
现在有\(n\)个水果，有\(m\)个人，他们每一个人会有两种需求，他们可能会需要第\(i\)种，也可能讨厌第\(j\)种
小A 讨厌\(a\) 喜欢\(b\)
小B 喜欢\(a\) 喜欢\(b\)
小C 讨厌\(a\) 讨厌\(b\)
显然无论如何选择\(ab\)都无法满足他们
我们不妨把两种要求设为 a,b,，变量前加 ¬ 表示「不」，即「假」。上述条件翻译成布尔方程即：\((¬ a∨b)\quad(a∨b)\quad(¬a∨¬b)\)
怎么求解 2-SAT 问题？
使用强连通分量
对于每个变量 \(x\)，我们建立两个点：\(x\quad¬x\), 分别表示变量 \(x\) 取 \(true\) 和取 \(false\)。所以，图的节点个数是两倍的变量个数。在存储方式上，可以给第 \(i\) 个变量标号为 \(i\)，其对应的反值标号为 \(i+n\)。对于每个同学的要求 \((a∨b)\)，转换为 \(¬a→b∧¬b→a\)。对于这个式子，可以理解为：「若 \(a\)不选则 \(b\) 必选，若 \(b\) 不选则 \(a\) 必选」然后按照箭头的方向建有向边就好了。综上，我们这样对上面的方程建图：
原式 \(\quad\quad\)建图
\((¬ a∨b)\quad a→b∧¬b→¬a\)
\((a∨b)\quad ¬a→b∧¬b→a\)
\((¬a∨¬b)\quad a→¬b∧b→¬a\)
说白了就是其中一个若不满足则另一个必须满足要求
建出来就长这样
通过图我们可以发现如果\(a\)成立则\(¬a\)也成立，这显然矛盾
那么我们通过一个强连通分量就可以判断矛盾情况是否可以相互到达
有了前置芝士，我们就可以看一道例题了
满汉全席
显然，\(n\)种肉相当于分别赋值为 满 或 汉。
对于\(j\) 评委（如汉式牛肉或满式羊肉)
就可以转化为 满式牛肉--->满式羊肉与汉式羊肉--->汉式牛肉
（ 类比上述\((¬ a∨b)\) ）
建好图后，开始\(Tarjan\)求强连通分量。可知，同一强联通分量中的菜不能包括同种肉的两种做法，否则，答案为\(BAD\)。所以求出强连通分量后，求可以立刻得出答案。
(样例一的建图)
点击查看代码
#include<bits/stdc++.h>
#define int long long
#define maxn 100010
using namespace std;
int head[maxn],low[maxn],dfs[maxn],Gro[maxn];
int vis[maxn];
int f,tot,cnt,group,num1,num2;
stack<int> q;
struct node{
int v,nex;}re[maxn];
void add(int u,int v)
{
++tot;
re[tot].v=v; re[tot].nex=head[u];
head[u]=tot;
}
void init()
{
memset(head,0,sizeof head);
memset(Gro,0,sizeof Gro);
memset(dfs,0,sizeof dfs);
memset(vis,0,sizeof vis);
memset(low,0,sizeof low);
f=tot=cnt=group=0;
num1=num2=0;
}
void tarjian(int x)
{
low[x]=dfs[x]=++cnt;
q.push(x); vis[x]=1;
for(int i=head[x];i;i=re[i].nex)
{
int v=re[i].v;
if(!dfs[v])
{
tarjian(v);
low[x]=min(low[x],low[v]);
}
else if(vis[v])
low[x]=min(low[x],dfs[v]);
}
if(low[x]==dfs[x])
{
int y;
group++;
do{
y=q.top();
q.pop(); vis[y]=0;
Gro[y]=group;
}
while(y!=x);
}
}
int T,n,m,k;
char s1[10],s2[10];
signed main()
{
scanf("%lld",&T);
while(T--)
{
scanf("%lld%lld",&n,&m);
init();
for(int i=1;i<=m;i++)// m 1~n h n+1~2n
{
cin>>s1>>s2;
k=1,num1=0;
while(s1[k]>='0'&&s1[k]<='9') num1=num1*10+s1[k++]-'0';
k=1,num2=0;
while(s2[k]>='0'&&s2[k]<='9') num2=num2*10+s2[k++]-'0';
if(s1[0]=='m')
{
if(s2[0]=='m') add(num1+n,num2),add(num2+n,num1);//分别是将h1连m2 同时将h2连m1
if(s2[0]=='h') add(num1+n,num2+n),add(num2,num1);//将h1连h2 同时将m2连m1
}
if(s1[0]=='h')
{
if(s2[0]=='m') add(num1,num2),add(num2+n,num1+n);
if(s2[0]=='h') add(num1,num2+n),add(num2,num1+n);
}
}
for(int i=1;i<=2*n;i++)
{
if(!dfs[i]) tarjian(i);
}
for(int i=1;i<=n;i++)
{
if(Gro[i]==Gro[i+n])
{
f=1; break;
}
}
if(f==1) printf("BAD\n");
else printf("GOOD\n");
}
return 0;
}
/*
2
3 4
m3 h1
m1 m2
h1 h3
h3 m2
2 4
h1 m2
m2 m1
h1 h2
m1 h2
*/