【模板】2-SAT问题

问题简述

有 (n) 个变量，每个变量可赋为 (1) 或 (0)
必须满足一些限制条件，如“ (a) 为1 或 (b) 为0 ” “ (a) 为0 且 (b) 为1” …
判断是否有一种赋值方法满足所有限制条件，并构造答案。

做法

首先拆点，把每个变量 (i) 拆成 (i) 选1 和 (i) 选0 两个点，在这两个点中选出一个
现在我们在 (2n) 个点中选出了 (n) 个点，相当于选择了一种赋值方案
换句话说，每种赋值方案就是在 每对 (i) 选1 和 (i) 选0 中选一个点

考虑所有限制条件，有两种类型。

第一种是 “ (x_i=k_i) 且 (x_j=k_j) ”
我们可以连一些有向边 ((u,v))，表示如果选了 (u) ，就一定要选 (v)
那针对这种情况，则要连 ((x_i选k_i, x_j选k_j))
但这样还不够！
回忆一下“逆否命题”，我们还需连 ((x_j不选k_j,x_i不选k_i)) 才可保证限制满足。

第二种是 “ (x_i=k_i) 或 (x_j=k_j) ”
连边 ((x_i不选k_i, x_j选k_j)) 和 ((x_j不选k_j,x_i选k_i))

这样下来，我们发现连的所有边是对称的！（真命题&逆否命题嘛）
接下来，我们对这个有向图跑强连通分量缩点。
对每个强连通分量，要么都选，要么都不选。

还记得如何选赋值方案吗？
每对(i) 选1 和 (i) 选0 中只能选1个，那么判断一下，如果这两个点在同一个强连通分量中，则无解。
如果不在，选拓扑排序中拓扑序靠后的那个点，（也就是 (tarjan) 中编号较小的那个点），可以保证这样选出的点是一组合理的赋值方案。

代码

洛谷模板题 (P4782)

#include<cstdio>
#include<iostream>
#include<algorithm>

using namespace std;

const int N = 2000005;

struct node{
    int v;
    node *nxt;
}pool[N],*h[N];
int cnt;
void addedge(int u,int v){
    node *p=&pool[++cnt];
    p->v=v;p->nxt=h[u];h[u]=p;
}

int n,m;

int tot;
int dfn[N],low[N],scc,belong[N];
int st[N],top,vis[N];
void tarjan(int u){
    int v;
    dfn[u]=low[u]=++tot;
    vis[u]=1;
    st[top++]=u;
    for(node *p=h[u];p;p=p->nxt)
        if(!dfn[v=p->v]){
            tarjan(v);
            low[u]=min(low[u],low[v]);
        }
        else if(vis[v]) low[u]=min(low[u],dfn[v]);
    if(low[u]==dfn[u]){
        scc++;
        while(1){
            belong[st[--top]]=scc;
            vis[st[top]]=0;
            if(st[top]==u) break;
        }
    }
}


int main()
{
    int a,b,c,d;
    scanf("%d%d",&n,&m);
    for(int i=0;i<m;i++){
        scanf("%d%d%d%d",&a,&b,&c,&d);
        addedge(a+(1-b)*n,c+d*n);
        addedge(c+(1-d)*n,a+b*n);
    }
    
    for(int i=1;i<=2*n;i++)
        if(!dfn[i]) tarjan(i);
    
    int flag=0;
    for(int i=1;i<=n;i++)
        if(belong[i]==belong[i+n]) flag=1;
    if(flag) { printf("IMPOSSIBLE
"); return 0; }
    printf("POSSIBLE
%d",belong[1]>belong[n+1]);
    for(int i=2;i<=n;i++) printf(" %d",belong[i]>belong[n+i]);
    
    return 0;
}