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

2-SAT

huunguyen Updated Tháng sáu 2, 2026

2-SAT (2-satisfiability) là bài toán: cho một công thức logic gồm nhiều mệnh đề (clause), mỗi mệnh đề là phép HOẶC của đúng 2 literal (một biến boolean hoặc phủ định của nó), hãy tìm cách gán giá trị true/false cho các biến sao cho mọi mệnh đề đều đúng — hoặc kết luận vô nghiệm. Trong khi 3-SAT (mỗi mệnh đề 3 literal) là NP-hard, 2-SAT lại giải được trong thời gian tuyến tính $O (V + E)$ nhờ quy về bài toán thành phần liên thông mạnh (SCC) trên một đồ thị kéo theo, thay vì thử $2^{n}$ tổ hợp gán.

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à một biến hoặc phủ định của một biến. Cần một phép gán thỏa mãn tất cả mệnh đề, hoặc báo vô nghiệm (UNSAT).

Ý tưởng / Trực giác

Bước 1 — Biến mệnh đề thành "kéo theo" (implication). Mệnh đề $(a \lor b)$ nghĩa là "ít nhất một trong hai đúng". Tương đương: nếu một cái sai thì cái kia buộc phải đúng. Viết bằng phép kéo theo:

$(a \lor b) ⟺ (\neg a \Rightarrow b) \land (\neg b \Rightarrow a)$

Trực giác: nếu $a$ sai mà mệnh đề vẫn phải đúng thì $b$ bắt buộc đúng — đó chính là một ràng buộc dây chuyền.

Bước 2 — Dựng đồ thị kéo theo (implication graph). Mỗi biến $x_{i}$ sinh ra hai đỉnh: đỉnh " $x_{i}$ đúng" và đỉnh " $x_{i}$ sai" ( $\neg x_{i}$ ). Mỗi kéo theo $u \Rightarrow v$ là một cạnh có hướng $u \to v$ . Như vậy mỗi mệnh đề thêm đúng 2 cạnh. Đường đi $u \to \dots \to w$ nghĩa là "chọn $u$ đúng thì kéo theo $w$ cũng phải đúng".

Bước 3 — Tính chất quyết định. Nếu trong đồ thị có đường đi $x_{i} \to \dots \to \neg x_{i}$ và $\neg x_{i} \to \dots \to x_{i}$ , thì hai đỉnh này nằm chung một chu trình, tức chung một SCC. Khi đó: gán $x_{i}$ đúng buộc $x_{i}$ sai (mâu thuẫn), gán $x_{i}$ sai cũng buộc $x_{i}$ đúng (mâu thuẫn). Vậy:

2-SAT vô nghiệm $⟺$ tồn tại biến $x_{i}$ mà $x_{i}$ và $\neg x_{i}$ nằm cùng một SCC.

Lý do hai cạnh được thêm "đối xứng" ( $\neg a \Rightarrow b$ và $\neg b \Rightarrow a$ ): nó đảm bảo đồ thị có tính đối ngẫu (skew-symmetry) — nếu có đường $u \to v$ thì luôn có đường $\neg v \to \neg u$ . Nhờ vậy $x_{i}$ và $\neg x_{i}$ không bao giờ cùng SCC một cách "ngẫu nhiên" trừ khi thực sự mâu thuẫn.

Bước 4 — Trích nghiệm từ thứ tự topo của các SCC. Co mỗi SCC thành một đỉnh, ta được một DAG (đồ thị không chu trình). Với mỗi biến, chọn literal nằm ở SCC đứng sau trong thứ tự topo (literal "đích" của các kéo theo). Lý do: kéo theo đi từ SCC sớm sang SCC muộn; chọn literal ở SCC muộn nghĩa là chọn cái mà mọi mũi tên đều trỏ tới, nên không kéo theo gì làm hỏng. Tarjan sinh SCC theo thứ tự topo ngược (SCC đánh số nhỏ là "muộn" hơn trong topo), nên quy tắc rút gọn lại thành: gán $x_{i} =$ true khi comp[x_i] < comp[¬x_i].

Ví dụ chạy tay

Xét $n = 2$ biến, 3 mệnh đề:

$(x_{0} \lor x_{1}) \land (\neg x_{0} \lor x_{1}) \land (\neg x_{0} \lor \neg x_{1})$

Quy ước mã hóa đỉnh: literal " $x_{i}$ đúng" $= 2 i$ , literal " $x_{i}$ sai" $= 2 i + 1$ . Phủ định = đảo bit cuối (^1). Vậy 4 đỉnh:

 đỉnh 0 = x0          đỉnh 1 = ¬x0
 đỉnh 2 = x1          đỉnh 3 = ¬x1

Thêm cạnh. Mệnh đề $(a \lor b)$ thêm $\neg a \to b$ và $\neg b \to a$ :

(x0 ∨ x1):    ¬x0→x1,  ¬x1→x0      tức 1→2, 3→0
(¬x0 ∨ x1):   x0 →x1,  ¬x1→¬x0     tức 0→2, 3→1
(¬x0 ∨ ¬x1):  x0 →¬x1, x1 →¬x0     tức 0→3, 2→1

Đồ thị kéo theo:

        0 (x0)
       / | \
      v  v  v        cạnh: 0→2, 0→3
     2   3  ...      1→2
     |   |           3→0, 3→1
     v   |           2→1
     1 <-+
   (¬x0)

  Danh sách kề:
   0 -> 2, 3
   1 -> 2
   2 -> 1
   3 -> 0, 1

Chạy Tarjan tìm SCC (đánh số SCC theo thứ tự kết thúc — topo ngược):

Thăm 0 -> 2 -> 1.  1 không còn cạnh mới (1->2, 2 đang trong stack)
  -> low[1] kéo về 2, low[2] kéo về 1: {1,2} là 1 vòng?
  Kiểm tra: 2->1->2  => {1,2} cùng SCC.   SCC #0 = {1,2}
  Quay lại 0 -> 3 -> 0 (3->0 đóng vòng với 0): {0,3} cùng SCC. SCC #1 = {0,3}

Kết quả comp (chỉ số SCC):

 đỉnh:  0    1    2    3
 comp:  1    0    0    1
        x0  ¬x0  x1  ¬x1

Kiểm tra vô nghiệm: với mỗi biến so comp[2i] và comp[2i+1]:

 x0: comp[0]=1, comp[1]=0  -> khác nhau  ✔ ổn
 x1: comp[2]=0, comp[3]=1  -> khác nhau  ✔ ổn

Không biến nào có hai literal chung SCC ⇒ có nghiệm.

Trích nghiệm (val[i] = comp[2i] < comp[2i+1]):

 x0: comp[0]=1 < comp[1]=0 ? 1<0 sai  -> x0 = false
 x1: comp[2]=0 < comp[3]=1 ? 0<1 đúng -> x1 = true

Kiểm chứng $x_{0} = F, x_{1} = T$ :

 (x0 ∨ x1)   = (F ∨ T) = T ✔
 (¬x0 ∨ x1)  = (T ∨ T) = T ✔
 (¬x0 ∨ ¬x1) = (T ∨ F) = T ✔

Cả 3 mệnh đề đúng — nghiệm hợp lệ.

Cài đặt

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

const int MAXN = 2e5 + 5;          // số biến tối đa
vector<int> adj[2 * MAXN];         // đồ thị kéo theo: 2 đỉnh / biến
int comp[2 * MAXN];                // chỉ số SCC của mỗi đỉnh
int disc[2 * MAXN], low[2 * MAXN]; // Tarjan: thời điểm thăm & low-link
int timer_val = 0, num_scc = 0;
bool on_stack[2 * MAXN];
stack<int> st;

// Tarjan tìm SCC; SCC được đánh số theo THỨ TỰ TOPO NGƯỢC
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]) {                 // cạnh cây
            dfs(v);
            low[u] = min(low[u], low[v]);
        } else if (on_stack[v]) {        // cạnh ngược/chéo về đỉnh còn trong stack
            low[u] = min(low[u], disc[v]);
        }
    }
    if (low[u] == disc[u]) {             // u là gốc một SCC
        while (true) {
            int v = st.top(); st.pop();
            on_stack[v] = false;
            comp[v] = num_scc;           // gán nhãn SCC
            if (v == u) break;
        }
        num_scc++;
    }
}

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

    // Mã hóa literal: x_i = true  -> đỉnh 2*i
    //                 x_i = false -> đỉnh 2*i + 1   (phủ định = ^1)
    // Thêm mệnh đề (a OR b): tương đương (¬a→b) và (¬b→a)
    void add_clause(int a, int b) {
        adj[a ^ 1].push_back(b);   // ¬a → b
        adj[b ^ 1].push_back(a);   // ¬b → a
    }

    // Ép biến i nhận giá trị val: dùng mệnh đề (l ∨ l)
    void set_val(int i, bool val) {
        int a = 2 * i + (val ? 0 : 1);
        add_clause(a, a);
    }

    bool solve(vector<bool>& val) {
        // reset trạng thái cho 2*n đỉnh
        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; // x_i và ¬x_i cùng SCC -> UNSAT
            // SCC chỉ số nhỏ = muộn hơn trong topo -> chọn literal ở đó
            val[i] = comp[2 * i] < comp[2 * i + 1];
        }
        return true;
    }
};

Ví dụ dùng (mỗi mệnh đề cho 4 số: chỉ số biến và giá trị literal mong muốn của mỗi vế):

int main() {
    int n, m; cin >> n >> m;
    TwoSat sat(n);
    for (int i = 0; i < m; i++) {
        int a, b; bool va, vb;
        cin >> a >> va >> b >> vb;   // (x_a == va) OR (x_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") << " ";
}

Mã hóa các ràng buộc thường gặp

Mọi ràng buộc dưới đây đều quy về mệnh đề 2-literal rồi gọi add_clause:

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}$ (bằng nhau)	$(x_{i} \lor \neg x_{j})$ và $(\neg x_{i} \lor x_{j})$
$x_{i} \neq x_{j}$ (khác nhau / XOR)	$(x_{i} \lor x_{j})$ và $(\neg x_{i} \lor \neg x_{j})$
"không cùng true" (NAND)	$(\neg x_{i} \lor \neg x_{j})$

Độ phức tạp

Thời gian: $O (V + E)$ với $V = 2 n$ đỉnh và $E = 2 m$ cạnh. Tarjan thăm mỗi đỉnh và duyệt mỗi cạnh đúng một lần (DFS), không quay lui lặp; vòng trích nghiệm cuối chạy $O (n)$ . Tổng $O (n + m)$ — tuyến tính theo kích thước công thức, thay vì $O (2^{n})$ của vét cạn.
Bộ nhớ: $O (V + E) = O (n + m)$ . Danh sách kề lưu $2 m$ cạnh; các mảng disc, low, comp, on_stack cùng stack Tarjan đều cỡ $2 n$ . Lưu ý mọi mảng phải khai báo theo $2 n$ (gấp đôi số biến) vì mỗi biến có 2 đỉnh.

⚠️ Lỗi thường gặp

Quên nhân đôi kích thước mảng. Mỗi biến tạo 2 đỉnh nên mọi mảng (adj, disc, comp, ...) phải cỡ $2 n$ , không phải $n$ . Triệu chứng: RuntimeError / truy cập ngoài biên hoặc kết quả sai khi $n$ lớn. Luôn đặt hằng MAXN rồi cấp phát 2 * MAXN.
Thêm sai/thiếu cạnh đối xứng. Mệnh đề $(a \lor b)$ cần cả hai cạnh $\neg a \to b$ và $\neg b \to a$ . Nếu chỉ thêm một cạnh, đồ thị mất tính skew-symmetry, kết luận SAT/UNSAT và nghiệm đều có thể sai. Mẹo: viết adj[a^1].push_back(b); adj[b^1].push_back(a); thành một cặp cố định.
Hiểu nhầm chiều thứ tự topo khi trích nghiệm. Tarjan đánh số SCC theo topo ngược: SCC chỉ số nhỏ đứng muộn hơn. Nếu dùng nhầm dấu so sánh (> thay vì <) bạn sẽ chọn literal sai và ra nghiệm vi phạm mệnh đề dù bài có nghiệm. Quy tắc đúng với cách cài này: val[i] = comp[2*i] < comp[2*i+1].
Đệ quy DFS tràn stack với $n$ lớn. Với $2 n$ tới vài trăm nghìn đỉnh, DFS đệ quy có thể stack overflow. Khắc phục: tăng giới hạn stack, hoặc viết Tarjan/Kosaraju khử đệ quy (dùng stack tường minh).
Quên reset trạng thái giữa nhiều testcase. Nếu chạy nhiều bộ test trong một lần, phải fill lại disc, low, comp, on_stack, xóa adj, đặt timer_val = num_scc = 0. Bỏ sót làm SCC của test sau bị "dính" dữ liệu test trước.
Ràng buộc "ép giá trị" bị quên hoặc sai. Để ép $x_{i} = true$ phải thêm $(x_{i} \lor x_{i})$ , tức cạnh $\neg x_{i} \to x_{i}$ (không có cạnh ngược lại). Nếu thêm nhầm thành cạnh hai chiều, bạn vô tình bắt $x_{i}$ và $\neg x_{i}$ vào cùng SCC ⇒ báo UNSAT giả.

Biến thể / Mở rộng

Trích nghiệm bằng Kosaraju (DFS hai lượt) thay cho Tarjan — cùng độ phức tạp, nhiều người thấy dễ nhớ hơn; thứ tự topo lấy từ thứ tự kết thúc lượt 1.
2-SAT có hướng dẫn (implication chains nâng cao): nhiều bài mô hình hóa ràng buộc "chọn 1 trong 2 vị trí/khe thời gian, hai đối tượng không đụng nhau" thành 2-SAT (mỗi đối tượng 1 biến boolean = chọn khe A hay B), ví dụ xếp lịch tránh xung đột, tô 2 màu có ràng buộc, đặt biển/quân cờ ở 1 trong 2 ô.
Nền tảng SCC. 2-SAT chỉ là một ứng dụng của co thành phần liên thông mạnh rồi xử lý trên DAG rút gọn. Nắm vững SCC (Tarjan/Kosaraju) và kỹ thuật co đồ thị + DP trên DAG là tiền đề để giải 2-SAT thành thạo.

Bài tập luyện

Pizza Khổng Lồ (giantpizza) — (Nâng cao) Bài 2-SAT kinh điển: mỗi người có 2 yêu cầu (thêm/bỏ topping), cần thỏa ít nhất một yêu cầu của mỗi người — mỗi người thành đúng một mệnh đề $(a \lor b)$ , áp thẳng khuôn mẫu ở trên.
Cánh đồng cỏ (grasscow) — (Kỳ cựu) Luyện nền tảng SCC + co đồ thị thành DAG mà 2-SAT dựa vào: tìm SCC, rút gọn rồi DP trên DAG để tối đa số trường thăm được khi cho đảo ngược một cạnh.

Ghi chú: kho bài CTOJ hiện chỉ có đúng một bài 2-SAT thuần (giantpizza); bài grasscow được thêm để luyện chắc kỹ thuật SCC/condensation — bước lõi mà 2-SAT xây trên. Sẽ cập nhật thêm bài 2-SAT khi kho có.