Hướng giải của Chuyển 2-CNF về đồ thị khả năng

Nhớ rằng hướng dẫn giải này chỉ nên sử dụng khi bế tắc, và tuyệt đối không nên sao chép mã nguồn kèm theo. Hãy tôn trọng tác giả bài tập và người viết hướng dẫn giải.
Nộp mã nguồn lời giải chính thức trước khi giải bài tập đó có thể khiến bạn bị ban.

Tác giả: kienadmin

Lời giải

Phân tích

Xây dựng đồ thị khả năng (implication graph) từ các mệnh đề 2-CNF:

  • Với mỗi mệnh đề \((a \lor b)\), thêm hai cạnh: \(\neg a \rightarrow b\) và \(\neg b \rightarrow a\).
  • Đồ thị có \(2N\) đỉnh và \(2M\) cạnh.

Sau đó tìm SCC bằng Kosaraju. Kiểm tra nếu tồn tại biến \(x\) và \(\neg x\) trong cùng SCC thì vô nghiệm.

In ra: YES/NO, số cạnh (\(2M\)), số SCC.

Độ phức tạp: \(O(N + M)\).

Mã nguồn C++

#include <bits/stdc++.h>
using namespace std;

int main() {
    ios_base::sync_with_stdio(false);
    cin.tie(NULL);
    int n, m;
    if (!(cin >> n >> m)) return 0;
    int sz = 2 * n + 2;
    vector<vector<int>> adj(sz), radj(sz);
    auto add_impl = [&](int u, int v) {
        adj[u].push_back(v);
        radj[v].push_back(u);
    };
    for (int i = 0; i < m; i++) {
        int a, b;
        if (!(cin >> a >> b)) return 0;
        int na = a > 0 ? 2 * a + 1 : 2 * (-a);
        int nb = b > 0 ? 2 * b + 1 : 2 * (-b);
        int a_node = a > 0 ? 2 * a : 2 * (-a) + 1;
        int b_node = b > 0 ? 2 * b : 2 * (-b) + 1;
        add_impl(na, b_node);
        add_impl(nb, a_node);
    }
    vector<int> order, comp(sz, 0);
    vector<bool> visited(sz, false);
    function<void(int)> dfs1 = [&](int u) {
        visited[u] = true;
        for (int v : adj[u]) if (!visited[v]) dfs1(v);
        order.push_back(u);
    };
    for (int i = 2; i <= 2 * n + 1; i++) if (!visited[i]) dfs1(i);
    int comp_id = 0;
    function<void(int)> dfs2 = [&](int u) {
        comp[u] = comp_id;
        for (int v : radj[u]) if (!comp[v]) dfs2(v);
    };
    for (int i = sz - 1; i >= 2; i--) {
        int u = order[i];
        if (!comp[u]) { comp_id++; dfs2(u); }
    }
    bool sat = true;
    for (int i = 1; i <= n; i++) {
        if (comp[2 * i] == comp[2 * i + 1]) { sat = false; break; }
    }
    cout << (sat ? "YES" : "NO") << "\n";
    cout << 2 * m << "\n";
    cout << comp_id << "\n";
    return 0;
}

Nhận xét

Không có ý kiến tại thời điểm này.