题解：P10969 Katu Puzzle

· · 题解

思路

前置芝士：P4782 【模板】2-SAT

将每个点拆为「TRUE」和「FALSE」两个点。

题目给出了 M 组关系，我们能发现对于每种关系，会有一些矛盾。如：X\vee Y=1，那么矛盾关系即为 \neg X \wedge \neg Y=1，所以如果我们选了 \neg X，那就只能选 Y 而不能选 \neg Y；同理，如果我们选了 \neg Y， 就只能选 X 而不能选 \neg X。

即如果有矛盾，则让有矛盾的两个状态，分别向另一个状态的“非”连一条边，通俗的来讲就是：

A\wedge B=0 \newline \Rightarrow (A\to \neg B),\ (B\to \neg A)

这也是很多 2-SAT 题用的连边方法，可以学习一下。

这时候又有人问了：驻波驻波，那如果我是 X\wedge Y = 1 或者 X \vee Y = 0 怎么办呢？

这种情况即为X=1\wedge Y=1 和 X=0\wedge Y = 0，那我们该如何规定 X 与 Y 的值呢？

我们考虑我们是如何确定一个点的值，我们比较 V 与 \neg V 的拓扑序，选定拓扑序大的一个。 所以我们如果想让 V 被选中，即令 V = 1 就是让 V 的拓扑序比 \neg V 大，那么我们就让 \neg V\to V，这样能保证 V 的拓扑一定会比 \neg V 大。

然后依照题目的要求进行建边，具体如何建边这里就不再赘述了，这种东西还是要自己想一想的。

最后再判断一下 X 和 \neg X 是否在同一个 scc 里即可。

AC code

#include<bits/stdc++.h>
using namespace std;
#define N 2005
int n, m;
vector<int> g[N];
int val(int x, int s) {
    if (s == 0) return x + n;
    return x;
}
int cnt, dfn[N], low[N], buc[N], scc[N], num;
stack<int> stk;
void Tarjan(int u) {
    dfn[u] = low[u] = ++cnt;
    stk.push(u);
    buc[u] = 1;
    for (auto v : g[u]) {
        if (!dfn[v]) {
            Tarjan(v);
            low[u] = min(low[u], low[v]);
        }
        else if (buc[v])
            low[u] = min(low[u], dfn[v]);
    }
    if (dfn[u] == low[u]) {
        int y;
        num++;
        do {
            y = stk.top();
            stk.pop();
            buc[y] = 0;
            scc[y] = num;
        } while (y != u);
    }
}
signed main() {
    cin >> n >> m;
    while (m--) {
        int a, b, c;
        string op;
        cin >> a >> b >> c >> op;
        a++;
        b++;
        if (op == "AND") {
            if (c) {
                g[val(a, 0)].push_back(val(a, 1));
                g[val(b, 0)].push_back(val(b, 1));
            }
            else {
                g[val(a, 1)].push_back(val(b, 0));
                g[val(b, 1)].push_back(val(a, 0));
            }
        }
        if (op == "OR") {
            if (c) {
                g[val(a, 0)].push_back(val(b, 1));
                g[val(b, 0)].push_back(val(a, 1));
            }
            else {
                g[val(a, 1)].push_back(val(a, 0));
                g[val(b, 1)].push_back(val(b, 0));
            }
        }
        if (op == "XOR") {
            if (c) {
                g[val(a, 1)].push_back(val(b, 0));
                g[val(b, 1)].push_back(val(a, 0));
                g[val(a, 0)].push_back(val(b, 1));
                g[val(b, 0)].push_back(val(a, 1));
            }
            else {
                g[val(a, 1)].push_back(val(b, 1));
                g[val(b, 1)].push_back(val(a, 1));
                g[val(a, 0)].push_back(val(b, 0));
                g[val(b, 0)].push_back(val(a, 0));
            }
        }
    }
    for (int i = 1; i <= 2 * n; i++)
        if (!dfn[i]) Tarjan(i);
    for (int i = 1; i <= n; i++) {
        if (scc[val(i, 0)] == scc[val(i, 1)]) {
            cout << "NO";
            return 0;
        }
    }
    cout << "YES";
    return 0;
}