标签：int Coel 笔记 ++ dfn maxn low SAT

终于结束网络流了，真有够累的……
接下来图论就还剩一点点了，加油~

SAT 问题相关概念

SAT 是 \(\mathcal{Satisfaction}\) 的英文缩写，意为“适应性”。对于若干个命题，每个命题都有且只有“真”和“假”两种取值。接下来会给出若干个条件，每个条件都形如“\(x_i\) 为真/假或 \(x_j\) 为真/假或……”的形式，需要找到一个命题取值，使得所有条件都可以得到满足。

如果一个条件关联了 \(k\) 个命题，就称为 K-SAT 问题。特殊地，每个条件只关联 \(2\) 个命题就叫 2-SAT 问题。

对于 \(k>2\) 的情况， SAT 问题是 \(\mathsf{NP}\) 完全的。但当 \(K=2\) 时，我们就可以以线性时间复杂度解决问题。

求解算法

在学习算法之前，我们先要了解一点数理逻辑的知识。

假设一个命题 \(a\) 是命题 \(b\) 的充分条件，即 \(a\to b\)，那么就会有 \(a\) 为真时 \(b\) 一定为真，\(a\) 为假时 \(b\) 可能为假。对于式子 \(a\to b\)，如果上面的情况正确就为真，反之为假。

为了更形象地了解这个“推导”的含义，下面给出了 \(a,b\) 不同的取值时 \(a\to b\) 的值。

写 Markdown 的时候上面一坨的 $ 看着好吓人

从上表可以发现， \(a\to b \iff \neg a \lor b\)，且 \(a\lor b \iff \neg a \to b \iff \neg b \to a\)。

我们可以把这个问题转化为图论问题。把所有命题放在一张有向图上，那么有向图的路径就代表了一个推导关系。接下来只要求解一个强连通分量就好了。

参考代码如下：

// Problem: 2-SAT 问题
// Contest: AcWing
// URL: https://www.acwing.com/problem/content/2404/
// Memory Limit: 512 MB
// Time Limit: 5000 ms
//
// Powered by CP Editor (https://cpeditor.org)

#include <algorithm>
#include <cstring>
#include <iostream>

using namespace std;

const int maxn = 4e6 + 10;

int n, m;
int head[maxn], nxt[maxn], to[maxn], cnt;
int dfn[maxn], low[maxn], stk[maxn], top;
int bel[maxn], vis[maxn], idx, tot;

void add(int u, int v) { nxt[cnt] = head[u], to[cnt] = v, head[u] = cnt++; }

void tarjan(int u) {
    dfn[u] = low[u] = ++tot;
    stk[++top] = u, vis[u] = true;
    for (int i = head[u]; ~i; i = nxt[i]) {
        int v = to[i];
        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]) {
        int v;
        idx++;
        do {
            v = stk[top--];
            vis[v] = false;
            bel[v] = idx;
        } while (v != u);
    }
}

int main(void) {
    ios::sync_with_stdio(false);
    cin.tie(nullptr);
    cin >> n >> m;
    memset(head, -1, sizeof(head));
    for (int i = 1; i <= m; i++) {
        int x, a, y, b;
        cin >> x >> a >> y >> b;
        x--, y--;
        add(2 * x + !a, 2 * y + b);
        add(2 * y + !b, 2 * x + a);
    }
    for (int i = 0; i < n * 2; i++)
        if (!dfn[i]) tarjan(i);
    for (int i = 0; i < n; i++)
        if (bel[i * 2] == bel[i * 2 + 1]) cout << "IMPOSSIBLE", exit(0);
    cout << "POSSIBLE" << '\n';
    for (int i = 0; i < n; i++)
        if (bel[i * 2] < bel[i * 2 + 1])
            cout << '0' << ' ';
        else
            cout << '1' << ' ';
    return 0;
}

标签：int,Coel,笔记,++,dfn,maxn,low,SAT
来源： https://www.cnblogs.com/Coel-Flannette/p/16487980.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。