2-SAT 略解

juruo999 · 2022-03-12 17:37:37 · 个人记录

2-SAT 问题

洛谷博客 github vercel

k-SAT

首先引入 k-SAT 问题。

k-SAT 问题说的就是有 n 个布尔值 a_i 和 m 组约束条件，其中每组约束都是 a 中 k 个值进行逻辑运算后等于一个给定值 （0 或 1） 的形式，求一组满足约束的 a_i（或者输出无解）。

比如

是一个 3-SAT 问题，它的一个解为

可以证明 k-SAT 在 k\ge3 时是没有多项式解法的，但是 k\le2 时有。

2-SAT

2-SAT 问题是 k-SAT 问题在 k=2 时的特例。

每一个约束条件都可以表示为 「a_i 为 x 或 a_j 为 y」的形式。和网络流一样，很多问题都可以建模为 2-SAT 问题，只要会求解 2-SAT，就可以解决许多问题。建模当然比原算法难哈哈哈

接下来是重点：如何求解 2-SAT 问题。

1. 图论建膜

先建立膜型 stO CYB Orz

我们把每个变量拆成两个点，一个表示该变量为真，另一个表示该变量为假。我们约定 \left<i,x\right> 为 a_i=x 代表的节点，如 \left<10,1\right> 表示 a_{10}=1 代表的节点。因此一个节点代表了一个命题。既然这样，我们就可以自然地定义节点 \left<i,x\right> 的非节点 \neg\left<i,x\right> 定义为 \left<i,\neg x\right>，表示 a_i\not= x 也就是 a_i=\neg x。

边表示蕴含关系，即 \left<i,x\right> 到 \left<j,y\right> 间有一条有向边表示如果 a_i=x 则 a_j=y。注意连边时要把这条边的逆否边连起来，\left<i,x\right> \to \left<j,y\right> 则 \left<j,\neg y\right> \to \left<i,\neg x\right>。为了方便，我们把 \left<i,x\right> 能走到 \left<j,y\right> 记为 \left<i,x\right> \Rightarrow \left<j,y\right>，走不到记为 \left<i,x\right> \not\Rightarrow \left<j,y\right>。

则原问题可化为：在约束对应的图上，选择 n 个点，使表示某变量为真与为假的点有且只有一个被选择，每个点若被选择，它能走到的节点也被选择。

2. 求解

怎么解呢？当然要请出我们的 爆搜 Tarjan 大佬。

首先我们发现，如果一个节点与它的非节点互相连通，那么问题肯定无解，因为如果 a_i=1\Rightarrow a_i=0 且 a_i=0\Rightarrow a_i=1，那么就形成了逻辑矛盾。

然后我们发现，如果 \left<i,x\right> \Rightarrow \left<i,\neg x\right> 且 \left<i,\neg x\right> \not\Rightarrow \left<i,x\right> 则 a_i=\neg x。（其实也就是反证法）

如果 \left<i,x\right> 与 \left<i,\neg x\right> 没有直接或间接关系，则 a_i 可以随便取值。

因此我们考虑将图用 tarjan 把强连通分量缩点，得到一张 DAG。如果一个点和它的非节点在同一个强连通分量中，则问题无解，否则，a_i 的取值就是 \left<i,1\right> 和 \left<i,0\right> 中缩点后拓扑序较小的节点，因为拓扑序较大的节点不可能走回拓扑序小的节点。

于是，我们得到了一组可行解。

code

// by juruo999
#include<iostream>
#include<cstdio>
#include<cstring>
#include<algorithm>
#include<vector>

using namespace std;

namespace sat{

    const int maxn=1000006;
    vector<int> e[maxn*2];

    int n;
    inline int rho(int i,bool x){   // <i,x>
        return i*2-x;
    }
    void add(int i,bool a,int j,bool b){    // x[i]==a => x[j]==b
        e[rho(i,a)].push_back(rho(j,b));
        e[rho(j,b^1)].push_back(rho(i,a^1));
    }

    int dfn[maxn*2],low[maxn*2],vis[maxn*2],cnt=0;
    int scc[maxn*2],sccn=0,stk[maxn*2],tp=0;
    void dfs(int u){
        low[u]=dfn[u]=++cnt;
        stk[++tp]=u;
        vis[u]=1;
        for(int i=e[u].size()-1;i>=0;i--){
            int v=e[u][i];
            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]){
            sccn++;
            while(stk[tp]!=u){
                vis[stk[tp]]=0;
                scc[stk[tp]]=sccn;
                tp--;
            }
            vis[stk[tp]]=0;
            scc[stk[tp]]=sccn;
            tp--;
        }
    }

    bool x[maxn];
    bool solve(){
        for(int i=1;i<=2*n;i++){
            if(!dfn[i]){ dfs(i); }
        }
        for(int i=1;i<=n;i++){
            if(scc[rho(i,0)]==scc[rho(i,1)]){
                return 0;
            }else{
                x[i]=scc[rho(i,0)]>scc[rho(i,1)];
            }
        }
        return 1;
    }

    bool& get(int i){
        return x[i];
    }

}

using sat::e;
using sat::rho;

int n,m;

int main(){

    scanf("%d%d",&n,&m);

    sat::n=n;
    for(int i=1;i<=m;i++){
        int x,a,y,b;
        scanf("%d%d%d%d",&x,&a,&y,&b);
        sat::add(x,a^1,y,b);
    }

    if(sat::solve()){
        puts("POSSIBLE");
        for(int i=1;i<=n;i++){
            printf("%d%c",sat::x[i]," \n"[i==n]);
        }
    }else{
        puts("IMPOSSIBLE");
    }

    return 0;

}

例题

模板题
双倍经验
NOI2017 游戏

第三题有一些难度，我做这道题的时候一开始建模建错了，结果不能保证每个地图都能分配到赛车……