Before \(2-SAT\)
一般形式为 \(k-适定性问题\)，简称 \(k-SAT\)
\(k>2\)为\(NP\)完全，暂不考虑，现考虑\(2-SAT\)
模型
有若干个包含2个元素的集合，只能选择每个集合中的一个元素，并给出一些条件（例：选a后不能选b），要求求出满足这些条件的选择，这个解也称为\(2-SAT\)的解
A B C
A' B' C'
若给出条件，{A,B'} , {B'C'} 不能同时选择
因为 {A,A'} , {B,B'} , {C,C'} 中，每个集合都要选出一个元素，即不能同时选择
又因为 {A,B'} 不能同时选择，则选择B'时，一定选择A'，于是在 B'，A' 之间连上一条有向边（因选 A' 不一定 B'）；同理，在选 B 时也一定选 A
于是可以建图
集合内元素是否矛盾就是\(Tarjan\)缩点之后，矛盾的元素是否在一个\(SCC\)
有，则不存在解
输出方案时可以通过变量在图中的拓扑序确定该变量的取值
我们可以发现，缩点后强连通分量的编号就是反着的拓扑排序
时间复杂度\(O(n+m)\)
非常的板，精髓在灵活建图
int head[N],nxt[N],to[N],tot=0;
int dfn[N],low[N],cnt=0;
int st[N],vis[N],pot[N],d[N],p[N],tp;
int n,m,t=0;
void add(int u,int v) {
nxt[++tot]=head[u];
to[tot]=v;
head[u]=tot;
}
void Tarjan(int u) {
low[u]=dfn[u]=++t;
st[++tp]=u;
vis[u]=1;
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(vis[v]) {
low[u]=min(low[u],low[v]);
}
}
if(dfn[u]==low[u]) {
int v;
cnt++;
while(v=st[tp--]) {
pot[v]=u;
vis[v]=0;
d[v]=cnt;
if(u==v) break;
}
}
}
bool fl=1;
signed main() {
n=read();
m=read();
for(int i=1;i<=m;i++) {
int u=read(),iu=read(),v=read(),iv=read();
add(u+(iu^1)*n,v+iv*n);//建图，以题意为准灵活更改
add(v+(iv^1)*n,u+iu*n);
}
for(int i=1;i<=n*2;i++) {
if(!dfn[i]) Tarjan(i);
}
//...
return 0;
}