2-SAT 问题

Tenshi · 2021-05-18 17:22:19 · 题解

k-SAT（全称Satisfiability）问题，具体来说，给定 n 个具有真假的命题，给一些逻辑关系（例如 p_1 \vee p_2），如果逻辑关系式子包含 k 个元，要求出 n 个命题的真假值满足所有逻辑关系。当 k>3 时，已经被证明为 NPC 问题，但是 k=2 时可以使用线性复杂度的算法解决，所以我们在这重点讨论 2-SAT 问题。

做法

注意到这样一个事实：a\vee b \Leftrightarrow \neg a \rightarrow b ，同理，a\vee b \Leftrightarrow \neg b \rightarrow a 。（详细可以参考数理逻辑）

如果将 n 个命题看成 2n 个点，然后利用上面的事实建边的话，就可以转化为图论问题求解了。

具体来说，例如，有命题 p_1,p_2 ，逻辑关系为 p_1\vee p_2 ，我们将 p_1 拆成两个状态（图论中相应的两个点） x_1, \neg x_1 ，分别表示 p_1 取真、取假，p_2 用相同方式处理，那么逻辑关系可以转化为图论中的两条有向边：(\neg x_1, x_2),~(\neg x_2, x_1) 。

用这样的方式，就可以将所给的命题以及逻辑关系转化为一个有向图了。

对这个有向图，我们采用 SCC缩点，如果一个命题的两个状态 x_i,~\neg x_i 同时出现在同一个强连通分量中，问题无解（因为不可能有 x_i 直接或间接地蕴含 \neg x_i）

否则，x_i,~\neg x_i 所在的强连通分量编号一定存在严格的偏序关系（通俗地说就是一定是一大一小），我们取编号小的那个状态作为命题 p_i 的取值即可。

下面简单说明这样取即可保证正确：

假如 \neg a \rightarrow b，由逆否命题性质，一定有 \neg b \rightarrow a ，如果说 \neg a 和 b 在同一强连通分量中，那么 \neg b 和 a 一定在另一强连通分量中，不妨设 a 所在的强连通分量编号较小，我们选取了 a 。由强连通分量性质，a 与 \neg b 可以相互到达，所以 \neg b 一定要被选取，而事实上由构造方式知 \neg b 一定是被选取的，因此这样做能够保证正确性。

具体细节参见代码。

在实现中，我们采取 tarjan 算法求强连通分量。

模板题

代码

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

inline void read(int &x) {
    int s=0;x=1;
    char ch=getchar();
    while(ch<'0'||ch>'9') {if(ch=='-')x=-1;ch=getchar();}
    while(ch>='0'&&ch<='9') s=(s<<3)+(s<<1)+ch-'0',ch=getchar();
    x*=s;
}

const int N=2e6+5, M=2e6+5;
int n, m;

struct node{
    int to, next;   
}e[M];

int h[N], tot;

void add(int u, int v){
    e[tot].to=v, e[tot].next=h[u], h[u]=tot++;
}

int ts, dfn[N], low[N];
int stk[N], top;
int id[N], cnt;
bool ins[N];

void tarjan(int u){
    dfn[u]=low[u]=++ts;
    stk[++top]=u, ins[u]=true;
    for(int i=h[u]; ~i; i=e[i].next){
        int go=e[i].to;
        if(!dfn[go]){
            tarjan(go);
            low[u]=min(low[u], low[go]);
        }else if(ins[go]) low[u]=min(low[u], dfn[go]);
    }

    if(dfn[u]==low[u]){
        int y;
        cnt++;
        do{
            y=stk[top--], ins[y]=false, id[y]=cnt; 
        }while(y!=u);
    }
}

int res[N];

int main(){
    memset(h, -1, sizeof h);
    read(n), read(m);

    while(m--){
        int i, a, j, b; read(i), read(a), read(j), read(b);
        i--, j--;
        add(2*i+!a, 2*j+b), add(2*j+!b, 2*i+a);
    }

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

    for(int i=0; i<n; i++) if(id[2*i]==id[2*i+1]){
        puts("IMPOSSIBLE");
        return 0;
    }else res[i]= id[2*i]>id[2*i+1];

    puts("POSSIBLE");
    for(int i=0; i<n; i++) printf("%d ", res[i]);
    cout<<endl;

    return 0;
}

2-SAT 问题

目录

简介

做法

代码