2 - SAT

定义

2 - SAT 指的是一种问题形式，通常表述为有 n 个集合，每个集合有且仅有两个元素，且集合之间有对应关系。

举个例子，假设有两个集合 \(A = \left \{a, b \right \}\) ， \(B = \left \{c, d \right \}\) ，存在对应关系 $ \neg a \to b \wedge a \to \neg b $ ， $ \neg c \to d \wedge c \to \neg d $ 。

通俗的讲就是满足在a成立时b不成立，a不成立时b成立，形如这种关系式的问题，一般被称为 2 - SAT

解法

该类题目一般是询问这 n 个集合的关系是否存在冲突，即是否成立，此时我们思考，不成立的状态显然是对于其中一个集合里的元素要同时满足两种状态，这显然是不可能的，那么如何解决呢？

考虑构建一个单向图，对关系式的两个元素进行连边，假设该关系式是 a ，b，两个值是异或关系，则让当 a 为真的时候 b 一定为假，反之亦然，那么就让 a1 连向 b0 ， a0 连向 b1 ，然后开始判断强连通分量，如果在一个强连通分量内同时存在 a1 与 a0 ，那么则不成立，因为在同一个 SCC 中，两个点互相可达，就会推出 a → ¬a 和 ¬a → a，这显然矛盾，所以无解。

所以 2 - SAT 的关键问题就是找出对应关系，然后建图跑SCC即可

例题不推荐先从洛谷的题目入手，洛谷的 2 - SAT 模板有些阴间，推荐从Codeforces的这道题入手比较模板。

示例代码：

#include<bits/stdc++.h>
using namespace std;
typedef long long ll;
const int N = 3e5 + 10;

ll dfn[N], low[N], sccId[N], door[N], key_to_door[N][2];
bool vis[N];
ll timer, sccCnt, n ,m;

stack<ll> s;
vector<ll> g[N];

void Tarjan(ll u){
    timer++;
    dfn[u] = low[u] = timer;
    vis[u] = true;
    s.push(u);
    for(auto v : g[u]){
        if(!dfn[v]){
            Tarjan(v);
            low[u] = min(low[u], low[v]);
        }
        else{
            if(vis[v]){
                low[u] = min(low[u], dfn[v]);
            }
        }
    }
    if(low[u] == dfn[u]){
        sccCnt++;
        while(1){
            ll t = s.top();
            s.pop();
            vis[t] = false;
            sccId[t] = sccCnt;
            if(u == t)break;
        }
    }
}



int main(){
    cin >> n >> m;
    for(int i = 1; i <= n; i++){
        cin >> door[i];
    }

    for(int i = 1; i <= m; i++){
        ll k = 0;
        cin >> k;
        for(int j = 1; j <= k; j++){
            ll x;
            cin >> x;
            if(key_to_door[x][0] == 0)key_to_door[x][0] = i;
            else key_to_door[x][1] = i;
        }
    }

    for(int i = 1; i <= n; i++){//这里将i设为真，i + m设为假，但其实真假在这道题里并没有作用
        if(door[i] == 0){
            g[key_to_door[i][0]].push_back(key_to_door[i][1] + m);
            g[key_to_door[i][1]].push_back(key_to_door[i][0] + m);
            g[key_to_door[i][0] + m].push_back(key_to_door[i][1]);
            g[key_to_door[i][1] + m].push_back(key_to_door[i][0]);
        }
        else{
            g[key_to_door[i][0]].push_back(key_to_door[i][1]);
            g[key_to_door[i][1]].push_back(key_to_door[i][0]);
            g[key_to_door[i][0] + m].push_back(key_to_door[i][1] + m);
            g[key_to_door[i][1] + m].push_back(key_to_door[i][0] + m);
        }
    }

    for(int i = 1; i <= m*2; i++){
        if(!dfn[i])Tarjan(i);
    }

    for(int i = 1; i <= m; i++){
        if(sccId[i] == sccId[i + m]){
            cout << "No\n";
            return 0;
        }
    }
    cout << "Yes\n";
    return 0;
}