Skip to content

2-sat ​

给定x1,x2,x3,x4,...,xn的bool值,以及多对aVb这样的形式,问是否存在一组解
根据离散数学的知识 $ a \vee b = \neg a \rightarrow b = \neg b \rightarrow a $

  • 建边后,tarjan缩点,选拓扑排序更靠后的点
  • 如果 $ x_i, \neg x_i $ 在一个强连通分量,则无解
  • tarjan缩点后编号即为拓扑排序逆序
cpp
int h[N],e[M],ne[M],idx;
void add(int a,int b){
    e[idx]=b,ne[idx]=h[a],h[a]=idx++;
}
int dfn[N],low[N],stk[N],id[N],timestamp,top,cnt;
bool in_stk[N];
void tarjan(int u){
    dfn[u]=low[u]=++timestamp;
    stk[++top]=u,in_stk[u]=1;
    for(int i=h[u];~i;i=ne[i]){
        int v=e[i];
        if(!dfn[v]){
            tarjan(v);
            low[u]=min(low[u],low[v]);
        }
        else if(in_stk[v])low[u]=min(low[u],dfn[v]);
    }
    if(low[u]==dfn[u]){
        int y;
        cnt++;
        do{
            y=stk[top--];
            in_stk[y]=0;
            id[y]=cnt;
        }while(y!=u);
    }
}
void solve(){
    int n,m;
    cin>>n>>m;
    memset(h,-1,sizeof h);
    while(m--){
        int i,a,j,b;
        cin>>i>>a>>j>>b;
        i--,j--;
        add(2*i+!a,2*j+b);
        add(2*j+!b,2*i+a);
    }
    for(int i=0;i<2*n;i++){
        if(!dfn[i])tarjan(i);
    }
    for(int i=0;i<n;i++){
        if(id[2*i]==id[2*i+1]){
            cout<<"IMPOSSIBLE\n";
            return;
        }
    }
    cout<<"POSSIBLE\n";
    for(int i=0;i<n;i++){
        if(id[2*i]<id[2*i+1])cout<<"0 ";
        else cout<<"1 ";
    }
}