「算法笔记」2-SAT 问题

一、定义

k-SAT（Satisfiability）问题的形式如下：

• 有 (n) 个 01 变量 (x_1,x_2,cdots,x_n)，另有 (m) 个变量取值需要满足的限制。

• 每个限制是一个 (k) 元组 ((x_{p_1},x_{p_2},cdots,x_{p_k}))，满足 (x_{p_1}oplus x_{p_2}opluscdotsoplus x_{p_k}=a)。其中 (a) 为 (0) 或 (1)，(oplus) 是某种二元 bool 运算（如 或运算 (vee)、与运算 (wedge)）。

• 要求构造一种满足所有限制的变量的赋值方案。

当 (k>2) 时该问题为 NP 完全的，只能暴力求解。因此一般讨论的是 (k=2) 的情况，即 2-SAT 问题。

二、基本思想

以 Luogu P4782 【模板】2-SAT 问题 为例，建立图论模型。

(m) 个限制，每个限制的形式都是 「(x_i) 为 真/假 或 (x_j) 为 真/假」。

对于变量 (x_i)，建立两个点 (i) 与 (i+n)，分别表示 (x_i) 为真、( eg x_i) 为真。

若 (x) 为真，则 ( eg x) 为假；若 ( eg x) 为假，则 (x) 为真。反之亦然。显然 (x) 和 ( eg x) 是互斥的。即，点 (i) 与 (i+n) 分别表示 (x_i) 为真或假。

对变量关系建有向图。有向边 (u o v) 表示，若 (u) 为真，则 (v) 一定为真。

具体地，对于每个限制 ((avee b))（变量 (a,b) 至少满足一个），可将其转化为 ( eg a ightarrow bwedge eg b ightarrow a)（(a) 为假则 (b) 一定为真；(b) 为假则 (a) 一定为真）。即节点 ( eg a) 向节点 (b) 连边，从节点 ( eg b) 向节点 (a) 连边。

考虑节点 (i) 与 (i+n) 在图中的关系。若它们 互相可达，即在 同一个强连通分量 中，则说明在赋值限制下，它们代表的一对互斥取值会同时被取到。则不存在一组合法的赋值方案。

否则，说明有解，考虑如何构造一组合法解。

首先，对建出的图进行缩点得到一个 DAG。考虑节点 (i) 与 (i+n) 所在强连通分量的 拓扑关系。若两分量不连通，则 (x_i) 取任意值（真或假）。否则只能取属于拓扑序较大的分量的值。因为若取拓扑序较小的值，可以根据逻辑关系推出取另一个值也是同时发生的。

三、具体实现

以 Luogu P4782 【模板】2-SAT 问题 为例。

1. 对于每个限制 ((avee b))（变量 (a,b) 至少满足一个），节点 ( eg a) 向节点 (b) 连边，从节点 ( eg b) 向节点 (a) 连边。

2. 用 Tarjan 算法对建出的图缩点。

3. 对于 (iin [1,n])，若 (i) 与 (i+n) 在同一个强连通分量中，则不存在一组合法的赋值方案。

4. 否则，根据 Tarjan 求得的强连通分量的标号为拓扑逆序（Tarjan 算法求强连通分量时使用了栈），即反向的拓扑序 ，可以得到 (x_i) 的值（取 (i) 与 (i+n) 所在强连通分量拓扑序较大的点的值）。

#include<bits/stdc++.h>
#define int long long
using namespace std;
const int N=2e6+5;
int n,m,x,a,y,b,cnt,hd[N],to[N<<1],nxt[N<<1],tot,c[N],top,s[N],num,dfn[N],low[N];
void add(int x,int y){
    to[++cnt]=y,nxt[cnt]=hd[x],hd[x]=cnt;
}
void tarjan(int x){
    dfn[x]=low[x]=++num,s[++top]=x;
    for(int i=hd[x];i;i=nxt[i]){
        int y=to[i];
        if(!dfn[y]) tarjan(y),low[x]=min(low[x],low[y]);
        else if(!c[y]) low[x]=min(low[x],dfn[y]);
    }
    if(low[x]==dfn[x]){
        c[x]=++tot;
        while(s[top]!=x) c[s[top--]]=tot;
        --top;
    }
}
signed main(){
    scanf("%lld%lld",&n,&m);
    for(int i=1;i<=m;i++){
        scanf("%lld%lld%lld%lld",&x,&a,&y,&b);
        if(a&&b) add(x+n,y),add(y+n,x);
        if(!a&&b) add(x,y),add(y+n,x+n);
        if(a&&!b) add(x+n,y+n),add(y,x);
        if(!a&&!b) add(x,y+n),add(y,x+n);
    }
    for(int i=1;i<=2*n;i++)
        if(!dfn[i]) tarjan(i);
    for(int i=1;i<=n;i++)
        if(c[i]==c[i+n]) puts("IMPOSSIBLE"),exit(0);
    puts("POSSIBLE");
    for(int i=1;i<=n;i++)
        printf("%d%c",c[i]<c[i+n],i==n?'
':' ');    //Tarjan 求得的强连通分量的标号为拓扑逆序，即反向的拓扑序 
    return 0;
}