2-SAT · Thuật toán Canuc80k

Có $n$ biến đúng/sai và nhiều điều kiện, mỗi điều kiện có dạng “ $a$ hoặc $b$ ” với $a$ , $b$ là một biến hay phủ định của nó. 2-SAT quyết định trong $O(n + m)$ có phép gán thỏa mọi điều kiện không, và dựng luôn phép gán. Mỗi điều kiện thành hai phép kéo theo, ta tìm thành phần liên thông mạnh trên đồ thị kéo theo. 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 được 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$ .

Hàng trên là xk, hàng dưới là ¬xk. 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.

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;
using 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)$ .

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ụ vô nghiệm: x1 kéo theo cả x3 lẫn ¬x3. Sửa một mệnh đề để có 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;
using 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+ - +

$O(n + m)$ .

Mỗi đối tượng một trong hai phương án

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;
using 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

$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;
using 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

$O(N^2)$ .

Khi đi thi

Thấy “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 bằng 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Ít nhất hai trong ba dự đoán đúng tương đương mỗi cặp trong ba có ít nhất một đúng: ba mệnh đề cho mỗi dòng.

LQDOJ

Bảng Điều Khiển Hai Công Tắccanuc80k7705Mỗi cửa cho một ràng buộc giữa hai công tắc của nó: bằng nhau nếu cửa đang mở, khác nhau nếu đang khóa.

LQDOJ

Ủy Ban Không Xung Độtcanuc80k7706Mỗi đoàn là một biến; hai đại biểu xung đột cho mệnh đề cấm. Ủy ban nhỏ nhất theo thứ tự: thử gán từng đoàn, lan truyền kéo theo bằng DFS, lỗi thì đổi đại biểu.

LQDOJ

Hướng Chiếu Đèncanuc80k7709Mỗi đèn chọn hàng hay cột; hai đèn cùng hàng cách nhau không quá

2r

không được cùng chọn hàng, tương tự với cột.

LQDOJ

Bảng Chọn Hai Kiểucanuc80k7710Mỗi món một biến hai kiểu; mỗi yêu cầu là một mệnh đề trực tiếp; nhiều bộ test, nhớ xóa đồ thị.

LQDOJ

Dựng Phép Gán Cho Công Thức Hai-CNFcanuc80k7712Như ví dụ dựng phép gán, in 1 và giá trị từng biến hoặc 0.

LQDOJ

Dãy Công Thức Liên Tiếpcanuc80k7713Nhiều công thức đến hết tệp; mỗi công thức dựng đồ thị và chạy Tarjan riêng.

LQDOJ

Các Cặp Trạng Thái Bị Cấmcanuc80k7714Hai trạng thái bị cấm cùng xuất hiện cho mệnh đề cấm trên hai literal tương ứng.

LQDOJ

Phân Nhóm Hai Phíacanuc80k7716Nhãn

0w

luôn thuộc nhóm: ép bằng clause(a, a); các điều kiện còn lại là mệnh đề hai nhãn.

LQDOJ

Chuỗi Nước Đi Không Thuacanuc80k7719Mỗi lượt có hai nước không thua; quan hệ giống hay khác giữa hai lượt cấm các cặp nước tương ứng.

LQDOJ

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

x

ở nhóm 0 kéo theo

a - x

ở nhóm 0, ở nhóm 1 kéo theo

b - x

ở nhóm 1; không có số bù thì ép nhóm kia.

LQDOJ

Bảng Chữ Cái Hai Tầngcanuc80k7724So hai từ liền kề ở vị trí khác đầu tiên: được ràng buộc kéo theo hoặc ép giữa các chữ được chọn ưu tiên.

LQDOJ

Các Dây Nối Quanh Vòngcanuc80k7725Hai dây đan chéo nhau trên vòng thì phải khác phía: mệnh đề khác nhau giữa hai biến.

LQDOJ

Hai Mốc Thời Giancanuc80k7728Chặt nhị phân khoảng cách nhỏ nhất; ở mỗi bước kiểm 2-SAT với các cặp thời điểm quá gần là xung đột.

LQDOJ

Bộ Thẻ Không Chung Ướccanuc80k7735Mỗi số nguyên tố cho một nhóm mặt thẻ chứa nó, chỉ được chọn tối đa một mặt; mã hóa “tối đa một” bằng biến tiền tố để số mệnh đề tuyến tính.

LQDOJ

Đọc thêm

2-SATVNOI WikiĐồ thị kéo theo, SCC và cách gán bằng tiếng Việt.
2-SATcp-algorithmsChứng minh và cài đặt bằng Kosaraju.
2-SATOI WikiMã hóa ràng buộc và bài mẫu.