2-SAT là gì: đồ thị kéo theo

Mỗi bạn trong lớp chọn đi dã ngoại hoặc ở nhà. Có những điều kiện kiểu: “An hoặc Bình phải đi”, “Bình và Chi không cùng đi”. Có cách chọn nào thỏa mọi điều kiện không?

Đó là 2-SAT: $n$ biến đúng/sai, mỗi điều kiện dạng “ $a$ hoặc $b$ ” với $a$ , $b$ là một biến hay phủ định của nó. Mỗi điều kiện thành hai phép kéo theo, và thành phần liên thông mạnh trên đồ thị kéo theo cho biết có nghiệm hay không, trong $O(n + m)$ , rồi dựng luôn phép gán. Phần lớn công sức nằm ở việc mã hóa đề thành các mệnh đề hai literal: chọn một trong hai phương án, không chọn cùng lúc hai thứ xung đột, các phép AND, OR, XOR.

Đồ thị kéo theo

Biến $x$ ứng với hai đỉnh: literal $x$ (số hiệu $2x$ ) và $\lnot x$ (số hiệu $2x + 1$ ; phủ định là u ^ 1). Mệnh đề $a \lor b$ tương đương hai phép kéo theo: nếu $a$ sai thì $b$ phải đúng, nếu $b$ sai thì $a$ phải đúng. Thêm cung $\lnot a \to b$ và $\lnot b \to a$ .

Mọi literal tới được từ $u$ trên đồ thị đều phải đúng khi $u$ đúng. Vì vậy nếu $x$ và $\lnot x$ nằm trong cùng một thành phần liên thông mạnh thì $x$ kéo theo $\lnot x$ và ngược lại: vô nghiệm. Điều ngược lại cũng đúng: không biến nào cùng thành phần với phủ định của nó thì luôn có nghiệm (phần dựng ở mục sau).

Ràng buộc khác đều viết được bằng mệnh đề: ép $a$ đúng là $a \lor a$ ; $a = b$ là $(a \lor \lnot b) \land (\lnot a \lor b)$ ; $a \ne b$ là $(a \lor b) \land (\lnot a \lor \lnot b)$ ; “không cùng $a$ và $b$ ” là $\lnot a \lor \lnot b$ .

Trong hình, hàng trên là $x_k$ , hàng dưới là $\lnot x_k$ . Mỗi bước thêm hai cung của một mệnh đề; cuối cùng tô thành phần mạnh và đọc phép gán.

Đồ thị kéo theo của các mệnh đề.

Hỏi nhanh

Mệnh đề $x_1 \lor \lnot x_2$ cho hai cung nào?

Ví dụMạng Phép Toán

Đề. $N \le 1000$ biến, $M \le 10^6$ ràng buộc $X_a \;op\; X_b = c$ với phép AND, OR hoặc XOR. Có phép gán thỏa hết không?

Lời giải. Mỗi ràng buộc dịch thành một hai mệnh đề hai literal:

AND bằng 1: ép $a$ đúng và ép $b$ đúng, tức $a \lor a$ và $b \lor b$ . AND bằng 0: không cùng đúng, $\lnot a \lor \lnot b$ .
OR bằng 1: $a \lor b$ . OR bằng 0: ép cả hai sai.
XOR bằng 1: $a \ne b$ , tức $(a \lor b) \land (\lnot a \lor \lnot b)$ . XOR bằng 0: $a = b$ , tức $(a \lor \lnot b) \land (\lnot a \lor b)$ .

Dựng đồ thị kéo theo trên $2N$ literal, tìm thành phần mạnh bằng Tarjan, vô nghiệm khi một biến nằm cùng thành phần với phủ định của nó.

Bước 1: literal và mệnh đề. Biến $x$ có đỉnh $2x$ (đúng) và $2x + 1$ (sai), nên phủ định là u ^ 1. clause(a, b) thêm hai cung $\lnot a \to b$ và $\lnot b \to a$ . clause(A, A) thêm cung $\lnot A \to A$ : nếu $A$ sai thì $A$ phải đúng, tức ép $A$ đúng.

C++

void clause(int a, int b) {
    g[a ^ 1].push_back(b);
    g[b ^ 1].push_back(a);
}

Bước 2: dịch ràng buộc theo đúng bảng trên.

C++

int A = 2 * a, B = 2 * b;
if (op == "AND") {
    if (c) clause(A, A), clause(B, B);
    else clause(A ^ 1, B ^ 1);
} else if (op == "OR") {
    if (c) clause(A, B);
    else clause(A ^ 1, A ^ 1), clause(B ^ 1, B ^ 1);
} else {
    if (c) clause(A, B), clause(A ^ 1, B ^ 1);
    else clause(A, B ^ 1), clause(A ^ 1, B);
}

Bước 3: Tarjan không đệ quy. Đồ thị có tới $4 \cdot 10^6$ cung nên không đệ quy. cs đóng vai ngăn xếp gọi hàm, it[u] nhớ đỉnh $u$ đã xét tới cung thứ mấy. Gặp đỉnh mới thì đẩy vào cả stk (ngăn xếp của Tarjan) và cs; gặp đỉnh đang trong stk thì cập nhật low[u] bằng tin[v]. Khi $u$ hết cung: bỏ $u$ khỏi cs, đưa low[u] lên cha (việc mà bản đệ quy làm sau khi lời gọi con trả về). Nếu low[u] == tin[u] thì $u$ là gốc của một thành phần mạnh: lấy khỏi stk mọi đỉnh tới $u$ .

C++

cs.pop_back();
if (!cs.empty()) low[cs.back()] = min(low[cs.back()], low[u]);
if (low[u] == tin[u]) {
    while (true) {
        int v = stk.back();
        stk.pop_back();
        onst[v] = 0, comp[v] = ncomp;
        if (v == u) break;
    }
    ncomp++;
}

Code đầy đủ

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

const int N = 2005;
int n, m, timer, ncomp, tin[N], low[N], comp[N], it[N];
bool onst[N];
vector<int> g[N];

void clause(int a, int b) {
    g[a ^ 1].push_back(b);
    g[b ^ 1].push_back(a);
}

void tarjan(int V) {
    vector<int> stk, cs;
    for (int s = 0; s < V; s++) {
        if (tin[s]) continue;
        cs.push_back(s);
        tin[s] = low[s] = ++timer, stk.push_back(s), onst[s] = 1;
        while (!cs.empty()) {
            int u = cs.back();
            if (it[u] < (int)g[u].size()) {
                int v = g[u][it[u]++];
                if (!tin[v]) {
                    tin[v] = low[v] = ++timer, stk.push_back(v), onst[v] = 1;
                    cs.push_back(v);
                } else if (onst[v]) low[u] = min(low[u], tin[v]);
            } else {
                cs.pop_back();
                if (!cs.empty()) low[cs.back()] = min(low[cs.back()], low[u]);
                if (low[u] == tin[u]) {
                    while (true) {
                        int v = stk.back();
                        stk.pop_back();
                        onst[v] = 0, comp[v] = ncomp;
                        if (v == u) break;
                    }
                    ncomp++;
                }
            }
        }
    }
}

signed main() {
    ios::sync_with_stdio(false);
    cin.tie(0);

    cin >> n >> m;
    for (int i = 0; i < m; i++) {
        int a, b, c;
        string op;
        cin >> a >> b >> c >> op;
        int A = 2 * a, B = 2 * b;
        if (op == "AND") {
            if (c) clause(A, A), clause(B, B);
            else clause(A ^ 1, B ^ 1);
        } else if (op == "OR") {
            if (c) clause(A, B);
            else clause(A ^ 1, A ^ 1), clause(B ^ 1, B ^ 1);
        } else {
            if (c) clause(A, B), clause(A ^ 1, B ^ 1);
            else clause(A, B ^ 1), clause(A ^ 1, B);
        }
    }
    tarjan(2 * n);
    bool ok = 1;
    for (int x = 0; x < n; x++)
        if (comp[2 * x] == comp[2 * x + 1]) ok = 0;
    cout << (ok ? "YES" : "NO") << '\n';
}

Input3 3
0 1 1 XOR
1 2 1 AND
0 2 1 OR

OutputYES

$O(N + M)$ . Đồ thị kéo theo có tới hàng triệu cung, nên cách lưu danh sách kề ảnh hưởng nhiều tới tốc độ:

Thành phần mạnh của đồ thị 400 nghìn đỉnh, 2 triệu cung, hai cách lưu cung.

Mảng cung liền nhau (đếm bậc, cộng dồn, điền cung) nhanh hơn vector<int> g[N] khoảng 6 lần, tính cả thời gian dựng đồ thị. Quy tắc: mệnh đề đọc hết trước được thì dựng đồ thị dạng mảng liền nhau.

Dựng phép gán

Co các thành phần mạnh được một DAG. Chọn cho mỗi biến literal nằm ở thành phần xuất hiện sau theo thứ tự tô pô: nếu chọn $x$ đúng trong khi $x \to \dots \to \lnot x$ thì mâu thuẫn, mà khi $x$ đứng sau $\lnot x$ thì không thể có đường từ $x$ tới $\lnot x$ . Tarjan đánh số thành phần theo thứ tự tô pô ngược (thành phần không có cung ra được đánh số trước), nên quy tắc là: $x$ đúng khi comp[2x] < comp[2x+1].

Với Kosaraju thì số hiệu đi theo thứ tự tô pô thuận và bất đẳng thức đổi chiều; luôn kiểm quy tắc với đúng thuật toán đang dùng.

Ví dụ dưới là vô nghiệm: $x_1$ kéo theo cả $x_3$ lẫn $\lnot x_3$ . Sửa một mệnh đề để có nghiệm.

Một hệ vô nghiệm.

Ví dụCấu Hình Tùy Chọn

Đề. $m \le 10^5$ tùy chọn, $n \le 10^5$ yêu cầu, mỗi yêu cầu gồm hai literal dạng + x hay - x, cần ít nhất một đúng. In +/- cho từng tùy chọn, hoặc IMPOSSIBLE.

Lời giải. Mỗi yêu cầu đã là một mệnh đề $a \lor b$ . Dựng đồ thị kéo theo trên $2m$ literal, chạy Tarjan, kiểm vô nghiệm như ví dụ trước (clause, tarjan giống hệt). Có nghiệm thì đọc phép gán: tùy chọn $x$ bật khi comp[2x] < comp[2x + 1].

Bước 1: đọc literal. + x là $2(x - 1)$ , - x là $2(x - 1) + 1$ .

C++

int a = 2 * (x1 - 1) + (s1 == '-'), b = 2 * (x2 - 1) + (s2 == '-');
clause(a, b);

Bước 2: đọc phép gán. Tarjan đánh số thành phần theo thứ tự xong; thành phần không có cung ra được đánh số trước, nên số nhỏ hơn là đứng sau trong thứ tự tô pô. Chọn literal ở thành phần đứng sau thì không có đường từ nó tới phủ định của nó, nên không kéo theo mâu thuẫn.

C++

for (int x = 0; x < m; x++) cout << (comp[2 * x] < comp[2 * x + 1] ? '+' : '-') << ' ';

Vì sao cả phép gán đều đúng: nếu một mệnh đề $a \lor b$ bị vi phạm thì cả $\lnot a$ và $\lnot b$ được chọn, mà có cung $\lnot a \to b$ , nên comp của $\lnot a$ không nhỏ hơn comp của $b$ . Ghép với các bất đẳng thức đã dùng để chọn $\lnot a$ và $\lnot b$ được một vòng bất đẳng thức nghiêm ngặt, vô lý.

Code đầy đủ

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

const int N = 2e5 + 5;
int n, m, timer, ncomp, tin[N], low[N], comp[N], it[N];
bool onst[N];
vector<int> g[N];

void clause(int a, int b) {
    g[a ^ 1].push_back(b);
    g[b ^ 1].push_back(a);
}

void tarjan(int V) {
    vector<int> stk, cs;
    for (int s = 0; s < V; s++) {
        if (tin[s]) continue;
        cs.push_back(s);
        tin[s] = low[s] = ++timer, stk.push_back(s), onst[s] = 1;
        while (!cs.empty()) {
            int u = cs.back();
            if (it[u] < (int)g[u].size()) {
                int v = g[u][it[u]++];
                if (!tin[v]) {
                    tin[v] = low[v] = ++timer, stk.push_back(v), onst[v] = 1;
                    cs.push_back(v);
                } else if (onst[v]) low[u] = min(low[u], tin[v]);
            } else {
                cs.pop_back();
                if (!cs.empty()) low[cs.back()] = min(low[cs.back()], low[u]);
                if (low[u] == tin[u]) {
                    while (true) {
                        int v = stk.back();
                        stk.pop_back();
                        onst[v] = 0, comp[v] = ncomp;
                        if (v == u) break;
                    }
                    ncomp++;
                }
            }
        }
    }
}

signed main() {
    ios::sync_with_stdio(false);
    cin.tie(0);

    cin >> n >> m;
    for (int i = 0; i < n; i++) {
        char s1, s2;
        int x1, x2;
        cin >> s1 >> x1 >> s2 >> x2;
        int a = 2 * (x1 - 1) + (s1 == '-'), b = 2 * (x2 - 1) + (s2 == '-');
        clause(a, b);
    }
    tarjan(2 * m);
    for (int x = 0; x < m; x++)
        if (comp[2 * x] == comp[2 * x + 1]) {
            cout << "IMPOSSIBLE\n";
            return 0;
        }
    for (int x = 0; x < m; x++) cout << (comp[2 * x] < comp[2 * x + 1] ? '+' : '-') << ' ';
    cout << '\n';
}

Input4 3
+ 1 + 1
- 2 - 2
+ 3 + 3
+ 1 - 2

Output+ - +

Độ phức tạp: $O(n + m)$ .

Chọn một trong hai

Dạng hay gặp nhất: mỗi đối tượng $i$ chọn phương án $0$ hoặc $1$ (một biến $x_i$ ), và một số cặp phương án của hai đối tượng xung đột không được cùng chọn. Với cặp xung đột ( $i$ chọn $p$ , $j$ chọn $q$ ), thêm mệnh đề $\lnot(x_i = p) \lor \lnot(x_j = q)$ . Duyệt mọi cặp đối tượng và mọi cặp phương án là $O(n^2)$ mệnh đề, đủ cho $n$ vài nghìn.

Khi cần tối ưu một ngưỡng (khoảng cách nhỏ nhất lớn nhất), chặt nhị phân ngưỡng và kiểm 2-SAT ở mỗi bước.

Hỏi nhanh

Cờ 1 đặt ở $3$ hoặc $13$ , cờ 2 ở $5$ hoặc $7$ , cần cách nhau ít nhất $8$ . Những cặp nào xung đột?

Ví dụCờ Trên Trục Số

Đề. $N \le 1000$ lá cờ, cờ $i$ đặt ở $X_i$ hoặc $Y_i$ ; mọi cặp cờ cách nhau ít nhất $D$ . In một cách đặt hoặc No.

Lời giải. Biến $x_i$ đúng là cờ $i$ đặt ở $X_i$ , sai là đặt ở $Y_i$ . Với mỗi cặp cờ $i < j$ và mỗi cặp phương án $(p, q)$ cách nhau dưới $D$ , hai lựa chọn đó không được cùng xảy ra: mệnh đề “không ( $i$ chọn $p$ ) hoặc không ( $j$ chọn $q$ )”. Tối đa $4 \binom{N}{2} \approx 2 \cdot 10^6$ mệnh đề, rồi 2-SAT như các ví dụ trước.

Bước 1: mệnh đề cấm. Literal 2 * i + p nghĩa là “cờ $i$ đặt ở pos[i][p]”. Cặp quá gần cho mệnh đề trên phủ định của cả hai lựa chọn. llabs vì hiệu tọa độ có thể âm.

C++

for (int i = 0; i < n; i++)
    for (int j = i + 1; j < n; j++)
        for (int p = 0; p < 2; p++)
            for (int q = 0; q < 2; q++)
                if (llabs(pos[i][p] - pos[j][q]) < d) clause((2 * i + p) ^ 1, (2 * j + q) ^ 1);

Bước 2: đọc phép gán như ví dụ trước: comp[2i] < comp[2i + 1] thì $x_i$ đúng, in pos[i][0], ngược lại in pos[i][1].

Code đầy đủ

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

const int N = 2005;
int n, timer, ncomp, tin[N], low[N], comp[N], it[N];
ll d, pos[N][2];
bool onst[N];
vector<int> g[N];

void clause(int a, int b) {
    g[a ^ 1].push_back(b);
    g[b ^ 1].push_back(a);
}

void tarjan(int V) {
    vector<int> stk, cs;
    for (int s = 0; s < V; s++) {
        if (tin[s]) continue;
        cs.push_back(s);
        tin[s] = low[s] = ++timer, stk.push_back(s), onst[s] = 1;
        while (!cs.empty()) {
            int u = cs.back();
            if (it[u] < (int)g[u].size()) {
                int v = g[u][it[u]++];
                if (!tin[v]) {
                    tin[v] = low[v] = ++timer, stk.push_back(v), onst[v] = 1;
                    cs.push_back(v);
                } else if (onst[v]) low[u] = min(low[u], tin[v]);
            } else {
                cs.pop_back();
                if (!cs.empty()) low[cs.back()] = min(low[cs.back()], low[u]);
                if (low[u] == tin[u]) {
                    while (true) {
                        int v = stk.back();
                        stk.pop_back();
                        onst[v] = 0, comp[v] = ncomp;
                        if (v == u) break;
                    }
                    ncomp++;
                }
            }
        }
    }
}

signed main() {
    ios::sync_with_stdio(false);
    cin.tie(0);

    cin >> n >> d;
    for (int i = 0; i < n; i++) cin >> pos[i][0] >> pos[i][1];
    for (int i = 0; i < n; i++)
        for (int j = i + 1; j < n; j++)
            for (int p = 0; p < 2; p++)
                for (int q = 0; q < 2; q++)
                    if (llabs(pos[i][p] - pos[j][q]) < d) clause((2 * i + p) ^ 1, (2 * j + q) ^ 1);
    tarjan(2 * n);
    for (int i = 0; i < n; i++)
        if (comp[2 * i] == comp[2 * i + 1]) {
            cout << "No\n";
            return 0;
        }
    cout << "Yes\n";
    for (int i = 0; i < n; i++) cout << (comp[2 * i] < comp[2 * i + 1] ? pos[i][0] : pos[i][1]) << '\n';
}

Input2 8
3 13
5 7

OutputYes
13
5

Độ phức tạp: $O(N^2)$ .

Khoảng thời gian xung đột

Mỗi sự kiện chọn một trong hai khoảng thời gian, hai khoảng được chọn không được giao nhau: đúng mẫu trên với “xung đột” là hai khoảng nửa mở $[l_1, r_1)$ , $[l_2, r_2)$ có $\max(l_1, l_2) < \min(r_1, r_2)$ . Đổi giờ phút ra số phút để so sánh, in ngược lại theo dạng hh:mm.

Ví dụLịch Nghi Lễ

Đề. $N \le 1000$ sự kiện, sự kiện $i$ từ $S_i$ tới $T_i$ , cần nghi lễ dài $D_i$ ở đầu ( $[S_i, S_i + D_i)$ ) hoặc cuối ( $[T_i - D_i, T_i)$ ). Các nghi lễ không được chồng nhau. In lịch hoặc NO.

Lời giải. Đổi giờ ra số phút. Biến $x_i$ đúng là nghi lễ ở đầu, $[S_i, S_i + D_i)$ ; sai là ở cuối, $[T_i - D_i, T_i)$ . Hai khoảng nửa mở giao nhau khi $\max(l_1, l_2) < \min(r_1, r_2)$ ; mỗi cặp giao nhau của hai sự kiện khác nhau cho một mệnh đề cấm, đúng khuôn của ví dụ cờ.

Bước 1: đổi giờ. toMin đổi hh:mm thành số phút; toStr làm ngược lại, in đủ hai chữ số bằng %02d. L[i][p], R[i][p] là khoảng của phương án $p$ ( $0$ là đầu, $1$ là cuối).

C++

int a = toMin(s), b = toMin(t);
L[i][0] = a, R[i][0] = a + d;
L[i][1] = b - d, R[i][1] = b;

Bước 2: mệnh đề cấm. Điều kiện giao nhau dùng đúng dạng nửa mở, nên hai nghi lễ nối đuôi nhau (một cái kết thúc đúng lúc cái kia bắt đầu) không bị coi là chồng.

C++

if (max(L[i][p], L[j][q]) < min(R[i][p], R[j][q])) clause((2 * i + p) ^ 1, (2 * j + q) ^ 1);

Phần 2-SAT và đọc phép gán giống ví dụ cờ; in lại khoảng đã chọn theo hh:mm.

Code đầy đủ

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

const int N = 2005;
int n, timer, ncomp, tin[N], low[N], comp[N], it[N], L[N][2], R[N][2];
bool onst[N];
vector<int> g[N];

void clause(int a, int b) {
    g[a ^ 1].push_back(b);
    g[b ^ 1].push_back(a);
}

void tarjan(int V) {
    vector<int> stk, cs;
    for (int s = 0; s < V; s++) {
        if (tin[s]) continue;
        cs.push_back(s);
        tin[s] = low[s] = ++timer, stk.push_back(s), onst[s] = 1;
        while (!cs.empty()) {
            int u = cs.back();
            if (it[u] < (int)g[u].size()) {
                int v = g[u][it[u]++];
                if (!tin[v]) {
                    tin[v] = low[v] = ++timer, stk.push_back(v), onst[v] = 1;
                    cs.push_back(v);
                } else if (onst[v]) low[u] = min(low[u], tin[v]);
            } else {
                cs.pop_back();
                if (!cs.empty()) low[cs.back()] = min(low[cs.back()], low[u]);
                if (low[u] == tin[u]) {
                    while (true) {
                        int v = stk.back();
                        stk.pop_back();
                        onst[v] = 0, comp[v] = ncomp;
                        if (v == u) break;
                    }
                    ncomp++;
                }
            }
        }
    }
}

int toMin(string s) {
    return stoi(s.substr(0, 2)) * 60 + stoi(s.substr(3, 2));
}

string toStr(int t) {
    char buf[8];
    sprintf(buf, "%02d:%02d", t / 60, t % 60);
    return buf;
}

signed main() {
    ios::sync_with_stdio(false);
    cin.tie(0);

    cin >> n;
    for (int i = 0; i < n; i++) {
        string s, t;
        int d;
        cin >> s >> t >> d;
        int a = toMin(s), b = toMin(t);
        L[i][0] = a, R[i][0] = a + d;
        L[i][1] = b - d, R[i][1] = b;
    }
    for (int i = 0; i < n; i++)
        for (int j = i + 1; j < n; j++)
            for (int p = 0; p < 2; p++)
                for (int q = 0; q < 2; q++)
                    if (max(L[i][p], L[j][q]) < min(R[i][p], R[j][q])) clause((2 * i + p) ^ 1, (2 * j + q) ^ 1);
    tarjan(2 * n);
    for (int i = 0; i < n; i++)
        if (comp[2 * i] == comp[2 * i + 1]) {
            cout << "NO\n";
            return 0;
        }
    cout << "YES\n";
    for (int i = 0; i < n; i++) {
        int p = comp[2 * i] < comp[2 * i + 1] ? 0 : 1;
        cout << toStr(L[i][p]) << ' ' << toStr(R[i][p]) << '\n';
    }
}

Input3
08:00 08:20 20
08:10 09:00 20
09:10 09:30 20

OutputYES
08:00 08:20
08:40 09:00
09:10 09:30

Độ phức tạp: $O(N^2)$ .

Khi đi thi

“Mỗi thứ chọn một trong hai”, “ít nhất một trong hai điều kiện”, ràng buộc giữa từng cặp: 2-SAT. Viết sẵn hàm clause(a, b) thêm hai cung, phủ định là ^ 1.
Ép một literal: clause(a, a). Bằng nhau, khác nhau, AND, OR, XOR đều là một hai mệnh đề.
Gán theo thứ tự thành phần mạnh: với Tarjan, $x$ đúng khi comp[x] < comp[¬x]. DFS không đệ quy khi số đỉnh lớn.

Tóm tắt

$a \lor b$ thành $\lnot a \to b$ và $\lnot b \to a$ .
Vô nghiệm khi và chỉ khi có $x$ cùng thành phần mạnh với $\lnot x$ .
Phép gán: chọn literal ở thành phần đứng sau theo thứ tự tô pô.
Xung đột giữa các cặp phương án thành mệnh đề cấm; tối ưu ngưỡng thì chặt nhị phân rồi kiểm.

Bài tập

Bảng Màu Ba Điều Kiệncanuc80k7704

LQDOJ

Bảng Điều Khiển Hai Công Tắccanuc80k7705

LQDOJ

Ủy Ban Không Xung Độtcanuc80k7706

LQDOJ

Hướng Chiếu Đèncanuc80k7709

LQDOJ

Bảng Chọn Hai Kiểucanuc80k7710

LQDOJ

Dựng Phép Gán Cho Công Thức Hai-CNFcanuc80k7712

LQDOJ

Dãy Công Thức Liên Tiếpcanuc80k7713

LQDOJ

Các Cặp Trạng Thái Bị Cấmcanuc80k7714

LQDOJ

Phân Nhóm Hai Phíacanuc80k7716

LQDOJ

Chuỗi Nước Đi Không Thuacanuc80k7719

LQDOJ

Phân Nhóm Theo Tổng Bùcanuc80k7722

LQDOJ

Bảng Chữ Cái Hai Tầngcanuc80k7724

LQDOJ

Các Dây Nối Quanh Vòngcanuc80k7725

LQDOJ

Hai Mốc Thời Giancanuc80k7728

LQDOJ

Bộ Thẻ Không Chung Ướccanuc80k7735

LQDOJ

Đọc thêm

2-SATVNOI Wiki
2-SATcp-algorithms
2-SATOI Wiki