2-SAT

Wiki › Thuật toán › Thuật toán đồ thị

huunguyen · Last updated 8, Tháng 4, 2026, 15:54

2-SAT là bài toán thỏa mãn (satisfiability) với mỗi mệnh đề chứa đúng 2 biến. Khác với 3-SAT (NP-hard), 2-SAT giải được trong $O (V + E)$ bằng SCC.

Bài toán

Cho $n$ biến boolean $x_{1}, \dots, x_{n}$ và $m$ mệnh đề dạng $(a \lor b)$ với $a, b$ là biến hoặc phủ định của biến. Tìm phép gán thỏa mãn tất cả mệnh đề (hoặc kết luận vô nghiệm).

Ý tưởng

Mỗi mệnh đề $(a \lor b)$ tương đương với hai hàm ý:

e g a \Rightarrow b và e g b \Rightarrow a

Xây đồ thị có hướng: mỗi biến $x_{i}$ có hai node $x_{i}$ và $\neg x_{i}$ , mỗi hàm ý là một cạnh.

Kết luận: 2-SAT vô nghiệm khi và chỉ khi tồn tại biến $x_{i}$ sao cho $x_{i}$ và $\neg x_{i}$ thuộc cùng một SCC.

Phép gán: Nếu có nghiệm, với mỗi biến $x_{i}$ : gán $x_{i} = true$ khi SCC của $x_{i}$ đứng sau SCC của $\neg x_{i}$ trong thứ tự topo của condensation graph (Tarjan đánh số ngược topo, nên so sánh chỉ số SCC).

Cài đặt

const int MAXN = 2e5 + 5;
vector<int> adj[2*MAXN];   // node i = x_i true, node i+n = x_i false
int comp[2*MAXN];          // SCC index (Tarjan: ngược topo)
int disc[2*MAXN], low[2*MAXN], timer_val = 0, num_scc = 0;
bool on_stack[2*MAXN];
stack<int> st;

void dfs(int u) {
    disc[u] = low[u] = ++timer_val;
    st.push(u); on_stack[u] = true;
    for (int v : adj[u]) {
        if (!disc[v]) { dfs(v); low[u] = min(low[u], low[v]); }
        else if (on_stack[v]) low[u] = min(low[u], disc[v]);
    }
    if (low[u] == disc[u]) {
        while (true) {
            int v = st.top(); st.pop();
            on_stack[v] = false;
            comp[v] = num_scc;
            if (v == u) break;
        }
        num_scc++;
    }
}

struct TwoSat {
    int n;
    TwoSat(int n) : n(n) {}

    // Thêm mệnh đề (a OR b)
    // a = 2*i   nếu x_i = true, a = 2*i+1 nếu x_i = false  (0-indexed)
    void add_clause(int a, int b) {
        adj[a ^ 1].push_back(b);   // ¬a → b
        adj[b ^ 1].push_back(a);   // ¬b → a
    }

    // Các loại ràng buộc thường gặp:

    // x_i = val (ép buộc)
    void set_val(int i, bool val) {
        int a = 2*i + (val ? 0 : 1);
        add_clause(a, a);   // (a OR a) tương đương buộc a = true
    }

    // x_i → x_j (nếu i thì j)
    void implies(int i, bool vi, int j, bool vj) {
        int a = 2*i + (vi ? 0 : 1);
        int b = 2*j + (vj ? 0 : 1);
        adj[a].push_back(b);       // a → b
        adj[b ^ 1].push_back(a ^ 1); // ¬b → ¬a
    }

    // Giải 2-SAT, trả về false nếu vô nghiệm
    // val[i] = giá trị của x_i nếu có nghiệm
    bool solve(vector<bool>& val) {
        fill(disc, disc + 2*n, 0);
        fill(on_stack, on_stack + 2*n, false);
        fill(comp, comp + 2*n, -1);
        timer_val = num_scc = 0;

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

        val.resize(n);
        for (int i = 0; i < n; i++) {
            if (comp[2*i] == comp[2*i+1]) return false;   // vô nghiệm
            // Tarjan: SCC nhỏ hơn = đứng sau trong topo
            val[i] = comp[2*i] < comp[2*i+1];
        }
        return true;
    }
};

Ví dụ sử dụng

int main() {
    int n, m; cin >> n >> m;
    TwoSat sat(n);

    for (int i = 0; i < m; i++) {
        // Mệnh đề: (x_a = va) OR (x_b = vb)
        int a, b; bool va, vb;
        cin >> a >> va >> b >> vb;
        sat.add_clause(2*a + (va ? 0 : 1), 2*b + (vb ? 0 : 1));
    }

    vector<bool> val;
    if (!sat.solve(val)) {
        cout << "UNSAT\n";
    } else {
        for (int i = 0; i < n; i++)
            cout << (val[i] ? "T" : "F") << " ";
    }
}

Các mệnh đề hay gặp

Ràng buộc	Mệnh đề tương đương
$x_{i} = true$	$(x_{i} \lor x_{i})$
$x_{i} = false$	$(\neg x_{i} \lor \neg x_{i})$
$x_{i} \Rightarrow x_{j}$	$(\neg x_{i} \lor x_{j})$
$x_{i} \Leftrightarrow x_{j}$	$(x_{i} \lor \neg x_{j})$ và $(\neg x_{i} \lor x_{j})$
$x_{i} \neq x_{j}$ (XOR)	$(x_{i} \lor x_{j})$ và $(\neg x_{i} \lor \neg x_{j})$
Ít nhất một trong ${x_{i}, x_{j}}$	$(x_{i} \lor x_{j})$

Khi nào dùng 2-SAT?

Bài toán chọn một trong hai lựa chọn cho mỗi đối tượng, thỏa mãn tập ràng buộc.
Bài toán tô màu 2 màu với ràng buộc.
Scheduling với xung đột: mỗi task có 2 khe thời gian, không được đụng nhau.

Bình luận

Không có bình luận tại thời điểm này.