这篇文章上次修改于 342 天前，可能其部分内容已经发生变化，如有疑问可询问作者。

ACM程序课算法笔记16——2-SAT

定义

SAT 是适定性（Satisfiability）问题的简称。一般形式为 k - 适定性问题，简称 k-SAT。对于n个集合，每个集合仅有两个元素。有存在元素矛盾，两个元素不能一起出现，两个元素不属于一个集合，问每个集合中选一个元素，判断能否选n个。找到其中的一个解决方案。

换个说法，有n个元素，每个元素都有两种状态，期中存在一些约束关系，比如A处于第一种状态的时候，B不能处于第二种状态。问是否能不冲突成立。

也就是存在多个布尔表达式，问是否存在情况使所有布尔表达式为真。

分析

为了便于解释，我们将每个元素的两种状态称为正反。

有点类似于小学奥数中推理问题，比如有条件A是正，B不能是正，我们就可以进行假设判定。如果A取正，那么B就只能取反。这就是一个推理过程，然后从B往后推，一旦推到A必须为反，就与假设矛盾了，也就不成立。

例如有条件：

种类①：A为正，即条件 A反 → A正 (直接使A必定为正)

种类②：A正时B不能为正，即条件 A正 → B反， B正 → A反

种类③：A == B 即条件 A正 → B正，A反 → B反，B正 → A正，B反 → A反

种类④：A ≠ B 即条件 A正 → B反，A反 → B正，B正 → A反，B反 → A正

注意！所有关系其逆否命题也必定成立，不能漏掉

建图

这就是一个推导条件，建立这些为边。

对于N个元素，图中有2N个点，这些点之间如果有这种推导关系就是建立了一个有向边

对于任意一个点，一旦我选择了其中一个点，这个点之后的路径走到的点就都要被取。

一旦取到的点属于同一个元素，说明当前取点不成立。

思路

暴搜

就是沿着图上一条路径，如果一个点被选择了，那么这条路径以后的点都将被选择，那么，出现不可行的情况就是，存在一个集合中两者都被选择了。

强联通分量缩点

引入强联通分量的概念，强联通分量在这个图中的意义是，属于一个强联通分量的点，一旦取了其中一个，那么其中所有的点都要被取。

先对图进行缩点，一旦一个缩点点集里面存在同一个元素的正反，就代表无解。

但如果没有这种冲突，该图就必定有解。

为什么必定有解

我们不妨探寻一下这个图的规律，由于种类①的边很有特色，我们不妨先排除这个种类。剩下的种类都有一个特点，其逆否命题和原命题组成了一对，而且逆否命题和原命题的边，两边的点均不一样。

如果我们多加几个点，这个图的样貌就很有特色

graph TB
 A1 --> B1
 B2 --> A2
 
 C1 --> A1
 A2 --> C2
 
 D1 --> A1
 A2 --> D2

 
 B1 --> E1
 E2 --> B2
 
 B1 -.-> C2
 C1 -.-> B2

这是一个关系的设定，我们的前提条件是已经缩了所有的环，所以此处无环。

由于逆否命题的特性：

该图必定有对称性。
所以对于任意一点例如A1A2，A1的后继和A2的前置必定对称
若问题无解，必定存在A1A2属于同一个环

根据对称性可证明，如果缩点点集不存在同一元素，则必定有解。

再回头考虑第一种联系，第一种联系是一个单向边，只要取被指向的那一组即可。

算法解决

先进行强联通分量的处理，判断缩点点集是否存在同一元素，如果没有，则有解。
如何得出结论，由拓扑排序的从后往前取即可

例题解决

party

#include<bits/stdc++.h>

using namespace std;

void solve(int n, int m){
    vector<int> G1[2 * n];// 图关系
    vector<int> G2[2 * n]; // 反图

    for(int i = 0; i < m; i++){
        int cuple1, cuple2, isHus1, isHus2;
        int oth1, oth2;
        cin >> cuple1 >> cuple2 >> isHus1 >> isHus2;
        int person1 = cuple1 * 2 + isHus1;
        int person2 = cuple2 * 2 + isHus2;
        
        if(isHus1 == 0)
            oth1 = person1 + 1;
        else
            oth1 = person1 - 1;
        
        if(isHus2 == 0)
            oth2 = person2 + 1;
        else
            oth2 = person2 - 1; 

        G1[person1].push_back(oth2);
        G1[person2].push_back(oth1);

        G2[oth2].push_back(person1);
        G2[oth1].push_back(person2);
    }

    vector<int> order;
    vector<bool> visited(2 * n);
    vector<int> sccValue(2 * n);

    function<void(int)> dfs1 = [&](int u){
        visited[u]= true;
        for(int v : G1[u]){
            if(not visited[v]) dfs1(v);
        }
        order.push_back(u);
    };

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

    int sccCnt = 0;

    function<void(int)> dfs2 = [&](int u){
        sccValue[u] = sccCnt;
        for(int v : G2[u]){
            if(not sccValue[v]) dfs2(v);
        }
    };

    for (int i = 2 * n - 1; i >= 0; i--){
        if (!sccValue[order[i]]) {
            ++sccCnt;
            dfs2(order[i]);
        }
    }

    bool success = true;
    for(int i = 0; i < n; i++){
        if(sccValue[2 * i] == sccValue[2 * i + 1]){
            success = false;
            break;
        }
    }

    if(success){
        cout << "YES" << endl;
    }else{
        cout << "NO" << endl;
    }

}

int main(){
    int n, m;
    while(cin >> n >> m){
        solve(n, m);
    }
}

Mai Icy