2-SAT

引子

有 \(2n\) 种药物，分成 \(n\) 对，每种药物恰好属于一对。现有一种治疗方法，每一对药至少吃一种，但有某些药不可以两个一起吃，求任意一种合法的吃药方案。

这样的现实问题可以转换为一个布尔方程组表示，设 \(a\)，\(a=1\) 表示吃 \(a\) 种药，\(a=0\) 表示不吃 \(a\) 种药。

在大多数问题中，用 \(a\) 表示 \(a=1\)，用 \(\neg a\) 来表示 \(a=0\)。

对于同一对的药，有： \(a=1\) 或 \(a'=1\)。

对于不可以一起吃的药，有：\(a=0\) 或 \(a^{''}=0\)。

即 \(a\) 或 \(a'\) ；\(\neg a\) 或 \(\neg a^{''}\)。

每一个这样的方程都需要成立至少一项。

求解这样的问题便可以使用 2-SAT。

思路

对于一个方程，我们考虑：如果前一项不成立，那么后一项必须成立；后一项不成立，那么前一项必须成立。

把每一个 \(a\) 和 \(\neg a\) 抽象成一个点。

于是对于一个方程 \(a\) 或 \(b\)，我们将 \(\neg a\) 到 \(b\) 和 \(\neg b\) 到 \(a\) 连有向边。

这条有向边的含义为：如果取 \(\neg a\) 那么必须取 \(b\)；如果取 \(\neg b\) 那么必须取 \(a\)。

对于一张图而言，如果形成了强联通分量，这个强联通分量上的点可以的取值构成一种合法的方案。

强连通的定义是：有向图 G 强连通是指，G 中任意两个结点连通。

强连通分量（SCC）的定义是：极大的强连通子图。

如果 \(a\) 和 \(\neg a\) 在同一个强联通分量内，方程无解。

因为不可以既取 \(a\) 又取 \(\neg a\)。

这里可以使用 Tarjin SCC 缩点（将一个分量缩成一个点），缩完点后，根据拓扑序求取值，如果 \(a\) 在 \(\neg a\) 之后，取 \(a\)；反之取 \(\neg a\)。可以证明（根据建图方法），如果每个都取后出现的点，在图有解的情况下，肯定存在一种方案。

CODE

P4782 【模板】2-SAT

#include<bits/stdc++.h>
using namespace std;

const int maxn=2e6+5;

struct node
{
    int to,nxt;
}edge[maxn*2];

int n,m,tot,dfntot,num;
int head[maxn],dfn[maxn],low[maxn],id[maxn];

bool vis[maxn];

stack<int>stk;

void add(int x,int y)
{
    tot++;
    edge[tot].to=y;
    edge[tot].nxt=head[x];
    head[x]=tot;
}

void dfs(int u)
{
    dfn[u]=low[u]=++dfntot,vis[u]=true,stk.push(u);
    for(int i=head[u];i;i=edge[i].nxt)
    {
        int v=edge[i].to;
        if(!dfn[v]) dfs(v),low[u]=min(low[u],low[v]);
        else if(vis[v]) low[u]=min(low[u],dfn[v]);
    }
    if(low[u]==dfn[u])
    {
        num++;
        while(stk.top()!=u) vis[stk.top()]=0,id[stk.top()]=num,stk.pop();
        vis[stk.top()]=0,id[stk.top()]=num;
        stk.pop();
    }
}

int main()
{
    scanf("%d%d",&n,&m);
    for(int i=1;i<=m;i++)
    {
        int x,a,y,b;
        scanf("%d%d%d%d",&x,&a,&y,&b);
        if(a==0&&b==1) swap(x,y),swap(a,b);
        if(a==0&&b==0) add(x,y+n),add(y,x+n);
        else if(a==1&&b==0) add(x+n,y+n),add(y,x);
        else if(a==1&&b==1) add(x+n,y),add(y+n,x);
    }

    for(int i=1;i<=n*2;i++) if(!dfn[i]) dfs(i);

    for(int i=1;i<=n;i++) if(id[i]==id[i+n]) printf("IMPOSSIBLE"),exit(0);
    printf("POSSIBLE\n");
    for(int i=1;i<=n;i++) cout<<(id[i]<id[i+n])<<" ";
}

END……