关于2-SAT

其实以前写过关于$2-SAT$的，但是那时的自己太懵懂了。

这是以前写过的文章link

关于$2-SAT$，其实就想说两件事情。

$2-SAT$边建立的逻辑

 $2-SAT$边建立的逻辑是必须关系，若$(u,v)$连边的话，说明如果要选择$u$号节点就必须要选择v号节点。

举个例子，假设有$2$个团队，若第一组团队编号为$(1,2)$，另一组编号为$(3,4)$

若$1,3$是仇人，则要连边$(1,4),(3,2)$，但是为什么不连$(4,1)$呢，因为不是如果要选择$4$就要选择$1$的，这是要必须关系

判断并输出解法

先说怎么判断有无解吧，就比如上个例子中$(1,2)$通过缩点后若在一个强连通分量中，则无解，因为若要选择$1$就要选择$2$，但是不能同时选择，所以无解。

现在就只剩有解的情况了，我们会发现一个问题，怎么去抉择呢。

首先，$tarjan$是拓扑序的倒序，这应该谁都懂吧。

然后呢，我们会发现若要选择的话应该选择出度最小的(应为此点没有对后来的点有限制)，就是建完反图后的入度为$0$的点。并且我们就是要选择出度最小的点吧，而$tarjan$又是反拓扑的，就是所在的$scc$小的吧，所以就每次选择$scc$最小的点即可。或许有人会质疑这个算法的正确性，第一就是刚才说的，第二就是我们会发现因为$scc$是从$1$开始的，所以说我们连边时进行传到过程中才是一个逐渐递增的过程。然后是不是什么都不用说了。

模板 $2-SAT$

link

#include<iostream>
#include<cstdio>
#include<cstring>
#include<algorithm>
#include<cmath>
using namespace std;
inline int read()
{
    int f=1,ans=0;char c;
    while(c<'0'||c>'9'){if(c=='-')f=-1;c=getchar();}
    while(c>='0'&&c<='9'){ans=ans*10+c-'0';c=getchar();}
    return ans*f;
}
const int N=1000001;
struct node{
    int u,v,nex;
}x[N<<3];
int head[N<<2],cnt,n,m,dfn[N<<2],low[N<<2],sta[N<<2],co[N<<2],col,tot,num;
void tarjan(int f){
    dfn[f]=low[f]=++num;
    sta[++tot]=f;
    for(int i=head[f];i!=-1;i=x[i].nex){
        if(!dfn[x[i].v]) tarjan(x[i].v),low[f]=min(low[f],low[x[i].v]);
        else if(!co[x[i].v]) low[f]=min(low[f],dfn[x[i].v]);
    }
    if(low[f]==dfn[f]){
        co[f]=++col;
        while(sta[tot]!=f){
            co[sta[tot]]=col;
            tot--; 
        }tot--;
    }return;
} 
void add(int u,int v){
    x[cnt].u=u,x[cnt].v=v,x[cnt].nex=head[u],head[u]=cnt++;
}
int opp(int pos,int x){
    if(x==0) return pos+n;
    return pos;
}
int st(int pos,int x){
    if(x==0) return pos;
    return pos+n;
}
bool judge(){
    for(int i=1;i<=2*n;i++)
        if(co[i]==co[i+n]) return 0;
    return 1;
}
int main(){
    memset(head,-1,sizeof(head));
    n=read(),m=read();
    for(int i=1;i<=m;i++){
        int p1=read(),u=read(),p2=read(),v=read();
        add(opp(p1,u),st(p2,v)),add(opp(p2,v),st(p1,u));
    }
    for(int i=1;i<=2*n;i++)
        if(!dfn[i]) tarjan(i);
    if(!judge()){printf("IMPOSSIBLE
");return 0;}
    printf("POSSIBLE
");
    for(int i=1;i<=n;i++){
        if(co[i]<co[i+n]) printf("0 ");
        else printf("1 ");
    }
}