Hướng giải của Kiểm tra biểu thức 2-SAT


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

Đây là bài toán 2-SAT kinh điển. Ta xây dựng đồ thị khả năng (implication graph) với \(2N\) đỉnh:

  • Đỉnh \(2i\) đại diện cho biến \(x_i\).
  • Đỉnh \(2i+1\) đại diện cho phủ định \(\neg x_i\).

Mỗi mệnh đề \((a \lor b)\) được thêm hai cạnh:

  • \(\neg a \Rightarrow b\)
  • \(\neg b \Rightarrow a\)

Sau đó, tìm thành phần liên thông mạnh (SCC). Nếu tồn tại biến \(x\) và \(\neg x\) trong cùng một SCC, bài toán vô nghiệm. Ngược lại, có nghiệm.

Độ 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); }
    }
    for (int i = 1; i <= n; i++) {
        if (comp[2 * i] == comp[2 * i + 1]) { cout << "NO\n"; return 0; }
    }
    cout << "YES\n";
    return 0;
}

Nhận xét

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