淺談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]);
}