Luogu P4782 模板2-SAT 问题(2-SAT)

Posted 2021-01-16 coder-uranus

P4782 【模板】2-SAT 问题

题意

题目背景

(2-SAT)问题模板

题目描述

有(n)个布尔变量(x_1sim 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,bin { 0,1} ))

输出格式：

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

输入输出样例

输入样例#1：

3 1
1 1 3 0

输出样例#1：

POSSIBLE
0 0 0

思路

快学(2-SAT)，这样你就可以做[NOI2017]游戏这道水题了。 --huyufeifei

(2-SAT)问题是我很喜欢的一类问题，一是因为它使用了我很喜欢的(Tarjan)算法
，二是它使用逻辑判断的方式实现的算法，这也是很使我喜欢的。

对于每一个(x_i)我们建两个点，编号为(i)和(i+n)，(i)表示(x_i=1)的情况，(i+n)表示(x_i=0)的情况。接下来考虑对于每一对逻辑关系建边。在这里，为了问题的普适性，我们不止考虑题目列出的条件，来试着考虑更多的情况。

• (a)为真：建立一条边((a+n,a))，表示如果(a)为假，则(a)为真。这样就可以最终推得(a)为真的情况。
• 如果(a)为真，则(b)为假：建立两条边：((a,b+n),(b,a+n))。
• (a)为真与(b)为假至少满足一个：建立两条边：((a+n,b+n),(b,a))。
• (a)为真与(b)为假不能同时满足：建立两条边：((a,b),(b+n,a+n))。

还有很多的情况没有枚举，不过它们与上述内容形似，在这里就不做列举了。

接下来怎么办呢？根据我们连边的方式，不难发现边的意义为推导出，也就是说，如果(a)能通过某些路径到达(b)，这表示的意义就是(a)能通过某些条件推导出(b)，那么如果我们让(a)满足，(b)就一定要被满足。如果(a,b)能够互达，就说明这两者要么同时被满足，要么同时不被满足。

不难想出，有且仅有一种情况无解：(a)与(a+n)可以互达，也就是两个互相矛盾的条件可以互相推导出。使用(Tarjan)缩点，这样可以快速求出任意两点是否可以互相到达，也就可以判断出解的存在性。

如何决定各个变量的取值呢？如果能从(a)推导出(a+n)，我们显然不能选择(a)，而只能选择(a+n)。所以对于同一个变量的两个取值，我们要检查其是否有推导的关系。根据(Tarjan)算法的特性，如果(a)能到达(b)且(a,b)不在同一缩出的点中，那么(b)缩点之后所在点的编号一定小于(a)。如果(a)不能到达(b)，那么两者的缩点编号不好判断。当然，既然只需要得出任意一组解，对于每一对((a,a+n))，我们就输出其缩点编号小的即可。

AC代码

#include<bits/stdc++.h>
using namespace std;
const int MAXN=2e6+5;
int n,m,tot,dfn[MAXN],low[MAXN];
int cnt,top[MAXN],to[MAXN],nex[MAXN];
int js,bel[MAXN];
bool vis[MAXN];
stack<int>S;
int read()
{
    int re=0;char ch=getchar();
    while(!isdigit(ch)) ch=getchar();
    while(isdigit(ch)) re=(re<<3)+(re<<1)+ch-'0',ch=getchar();
    return re;
}
void add_edge(int x,int y){to[++cnt]=y,nex[cnt]=top[x],top[x]=cnt;}
void tarjan(int now)
{
    dfn[now]=low[now]=++tot,vis[now]=true;
    S.push(now);
    for(int i=top[now];i;i=nex[i])
        if(!dfn[to[i]]) tarjan(to[i]),low[now]=min(low[now],low[to[i]]);
        else if(vis[to[i]]) low[now]=min(low[now],dfn[to[i]]);
    if(dfn[now]==low[now])
    {
        bel[now]=++js,vis[now]=false;
        while(S.top()!=now) bel[S.top()]=js,vis[S.top()]=false,S.pop();
        S.pop();
    }
}
int main()
{
    n=read(),m=read();
    while(m--)
    {
        int x=read(),xx=read(),y=read(),yy=read();
        if(xx&&yy) add_edge(x+n,y),add_edge(y+n,x);
        else if(xx&&!yy) add_edge(x+n,y+n),add_edge(y,x);
        else if(!xx&&yy) add_edge(x,y),add_edge(y+n,x+n);
        else if(!xx&&!yy) add_edge(x,y+n),add_edge(y,x+n);
    }
    for(int i=1;i<=(n<<1);i++) if(!dfn[i]) tarjan(i);
    for(int i=1;i<=n;i++)
        if(bel[i]==bel[i+n])
        {
            printf("IMPOSSIBLE");
            return 0;
        }
    puts("POSSIBLE");
    for(int i=1;i<=n;i++) printf("%d ",bel[i]<bel[i+n]);
    return 0;
}