浅谈2-SAT

引入：

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

其实\(2-SAT\)的题目描述和这个很像（虽然解法不同）

那么\(2-SAT\)究竟是什么呢？

首先，把\(2\)和\(SAT\)拆开。\(SAT\) 是 \(Satisfiability\) 的缩写，意为可知足性。即一串布尔变量，每一个变量只能为真或假。要求对这些变量进行赋值，知足布尔方程(摘自\(Anguei\)的题解)

通俗一点来讲，就是有\(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]);
}