题解 P4782 【【模板】2-SAT 问题】

· · 题解

博客阅读更佳

SAT问题的定义

SAT是Satisfiability（可满足性）的缩写，而k-SAT问题就是说你有n个未知的bool变量a_i，有m个对这些变量的限制，每个限制有k个元素，设每个元素为x，要求 x或\neg x 的 \lor（或）或者\land（和）的值（如3-SAT中，形如(a or b or !c) 或 a and !b and !c 的条件）为true，或定义某一个未知数为true/false的一种解法。

很容易想到O(2^nm)暴力做法，即枚举每一个bool未知数的值，判断是否合法。而对于k \geq 3而言的k-SAT已经被证明是NP完全问题（即没有多项式复杂度的问题），而我们研究的2-SAT则有一个多项式解法。

2-SAT问题的解法

定义对于任何一个单字母bool变量a为true。

我们通过建一些特殊的图来实现：我们令编号从1到n的点为未知变量a_i取true的情况，n+1到2 \times n的点为a_i取false的情况。连边方面，我们令从a连向b表示由a能推到b，则a\land b可以变为a \rightarrow b, b\rightarrow a，即由a为真可以推出b为真，由b为真可以推出a为真；a \lor b可以变为\neg a \rightarrow b, \neg b \rightarrow a，即若a为假则b为真；a = x (x\in \{ true, false\})可以变为\neg a \rightarrow a，这个我们之后再说为什么，先当这种情况不存在。可以发现所有情况都可以化为刚才三种情况之一。

然后我们对于这样一个特殊的图跑一边强连通分量，如果存在\neg a和a只有同存在于同一个强连通分量中，则一定无解，因为这一意味着你可以从\neg a推到a，而很明显这是矛盾的。

于是我们得到了一张拓扑图。有一个性质，就是在有解的情况下，一个未知数的两个取值是有前后推导关系的，也就是一个取值直接或间接的指向了另一个取值时，我们取后者是一定有解的。实际实现上，输出的时候，输出对于每一个点拆除的true和false中，拓扑序较大的那一个，则一定有一个解。然而由于我们跑了Tarjan，那么我们可以附带着求一个反向的拓扑序，那么这就拓扑序也求得了。

从刚才这一角度来说，对于刚才建图中的第三种情况，我们连\neg a \rightarrow a可以让a的拓扑序必定大于\neg a，即最后输出的时候一定会输出开始时给它的定义。

很明显复杂度瓶颈在Tarjan跑强连通分量上，其复杂度为O(n+m)，所以总复杂度为O(n+m)

例题

例题1 P4782 【模板】2-SAT 问题

一道模板题，甚至连赋值操作都没有。可以看到这里输入的时候用了一些小技巧来压了一下输入的行，其他就没什么难以理解的了。

#include <iostream>
#include <cstdio>
#include <cstring>
#include <algorithm>
#include <vector>
namespace ztd{
    using namespace std;
    typedef long long ll;
    const int mod = 998244353;
    const int inf = 2147483647;
    template<typename T> inline T read(T& t) {//fast read
        t=0;short f=1;char ch=getchar();double d = 0.1;
        while (ch<'0'||ch>'9') {if (ch=='-') f=-f;ch=getchar();}
        while (ch>='0'&&ch<='9') t=t*10+ch-'0',ch=getchar();
        if(ch=='.'){ch=getchar();while(ch<='9'&&ch>='0') t+=d*(ch^48),d*=0.1,ch=getchar();}
        t*=f;
        return t;
    }
}
using namespace ztd;
const int maxn = 2e6+7, maxm = 2e6+7;
int n, m;

int last[maxn], ecnt;
struct edge{int y, gg;}e[maxm];
inline void addedge(int x, int y){
    e[++ecnt] = {y, last[x]};
    last[x] = ecnt;
}

int dfn[maxn], low[maxn], pcnt, st[maxn], top, gang[maxn], gtot;
bool instack[maxn];
void Tarjan(int x){
    dfn[x] = low[x] = ++pcnt; 
    st[++top] = x; instack[x] = 1;
    for(int i = last[x], y = e[i].y; i; i = e[i].gg, y = e[i].y){
        if(!dfn[y]){
            Tarjan(y);
            low[x] = min(low[x], low[y]);
        }else if(instack[y]) low[x] = min(low[x], dfn[y]);
    }
    if(low[x] == dfn[x]){
        int now; ++gtot;
        do{
            now = st[top--]; instack[now] = 0;
            gang[now] = (gtot);
        }while(now ^ x);
    }
}

int main(){
    read(n); read(m);
    int xx, yy, hmx, hmy;
    for(int i = 1; i <= m; ++i){
        read(xx); read(hmx); read(yy); read(hmy); 
        addedge(xx+(1-hmx)*n, yy+hmy*n);
        addedge(yy+(1-hmy)*n, xx+hmx*n);
    }
    for(int i = 1; i <= n*2; ++i) if(!dfn[i]) Tarjan(i);
    for(int i = 1; i <= n; ++i){
        if(gang[i] == gang[i+n]){
            puts("IMPOSSIBLE");
            return 0;
        } 
    }
    puts("POSSIBLE");
    for(int i = 1; i <= n; ++i){
        cout << ((int)(gang[i] > gang[i+n])) << " ";
    } 
    cout << '\n';
    return 0;
}

还有几道比较好的练手题，如

P4171 【JSOI2010】满汉全席（跟模板区别不大）

P3825 【NOI2017】游戏（比较好的实际应用题）

关于这些题的题解，可以在我的博客里看。