题解 P4782 【【模板】2-SAT 问题】

· · 题解

引入：

相信大家都了解过差分约束系统。差分约束系统的大体意思就是给出一些有某种关系的变量，问你是否有某种赋值使得这些关系全部成立

其实2-SAT的题目描述和这个很像（虽然解法不一样）

那么2-SAT到底是什么呢？

通俗一点来说，就是有n个bool变量x_1~x_n有m个位运算的表达式（只有两个变量），求是否有一种方法使得m个表达式都成立

\

例题

洛谷P4782

题目背景

2-SAT 问题 模板

题目描述

有n个布尔变量x_1~x_n，另有m个需要满足的条件，每个条件的形式都是"x_i为true/false"或"x_j为true/false"。比如"x_1为真或x_3为假"、"x_7为假或x_2为假"。2-SAT 问题的目标是给每个变量赋值使得所有条件得到满足。

输入格式

第一行两个整数n和m，意义如体面所述。

接下来m行每行4个整数 i ,a, j, b ，表示"x_i为a或x_j为b"(a,b\in \{0,1\}​)

输出格式

如无解，输出"IMPOSSIBLE"（不带引号）; 否则输出"POSSIBLE"（不带引号),下一行n个整数（x_1~x_n\in \{0,1\}），表示构造出的解。

\

如何解决这类问题？

首先，我们发现一个变量取值的真和假是相对独立的，也就是说和他自己没有关系，只和其他变量的真假有关系

那我们不妨为每一个变量建两个节点，一个表示真，一个表示假（我这里用1~n表示假，n+1~2n表示真）

有了点，考虑怎么连边。如果一个变量的真假能够推出另一个变量的真假，就对这两个变量对应的真假连边

比如：x_1为真或x_2为假，那么x_1的假就可以推出x_2的真，x_2的真就可以推出x_1的假

那么就把x_1对应的假节点连向x_2对应的真节点，把x_2对应的真节点连向x_1对应的假节点

如何判断有没有解？

考虑无解的情况，肯定是出现了矛盾，也就是一个点的真推出了它自己的假，或者是这个点的假推出了它自己的真。这种情况有什么特征？

发现如果是这样的话，这个点的真和假一定在相同的强连通分量里面

强联通分量？那不就是tarjan吗？

时间复杂度O(n+m)

那么怎么找出满足题意的解？

当x所在的强连通分量的拓扑序在\neg x之后时，直接取x为真就行了。tarjan算法在执行的过程中已经为每一个强连通分量标好了拓扑序（不过是和正常的拓扑序相反）

#include<bits/stdc++.h>
using namespace std;
const int N=2000050;

int head[N],ecnt;//1~n存0,n+1~2n存1 
struct edge
{
    int to,nxt;
}edg[N<<1];

inline void add(int u,int v)
{
    edg[++ecnt].to=v;
    edg[ecnt].nxt=head[u];
    head[u]=ecnt;
}

int n,m;

inline void read()
{
    for(int i=1;i<=m;i++)
    {
        int x,a,y,b;
        scanf("%d%d%d%d",&x,&a,&y,&b);//建边 
        if(a==1&&b==1) add(x,y+n),add(y,x+n);
        if(a==0&&b==1) add(x+n,y+n),add(y,x);
        if(a==1&&b==0) add(x,y),add(y+n,x+n);
        if(a==0&&b==0) add(x+n,y),add(y+n,x);
    }
}
//tarjan
int dfn[N],low[N],in[N],s[N],scc[N],top,ind,cnt;

void tarjan(int x)
{
    low[x]=dfn[x]=++ind;
    s[top++]=x;
    in[x]=1;
    for(int i=head[x];i;i=edg[i].nxt)
    {
        int v=edg[i].to;
        if(!dfn[v])
        {
            tarjan(v);
            low[x]=min(low[x],low[v]);
        }
        else if(in[v]) low[x]=min(low[x],dfn[v]);
    }
    if(dfn[x]==low[x])
    {
        cnt++;
        while(s[top]!=x)
        {
            top--;
            in[s[top]]=0;
            scc[s[top]]=cnt;
        }
    }
}

int main()
{
    scanf("%d%d",&n,&m);
    read();
    for(int i=1;i<=2*n;i++)
    {
        if(!dfn[i]) tarjan(i);
    }
    for(int i=1;i<=n;i++) if(scc[i]==scc[i+n]) return cout<<"IMPOSSIBLE",0;
    puts("POSSIBLE");
    for(int i=1;i<=n;i++) printf("%d ",scc[i]>scc[i+n]);
}