2-SAT

IBài toán 2-SAT và cách thử hết

Một biến logic nhận một trong hai giá trị: đúng hoặc sai. Với biến $x$, ta viết $\lnot x$ (đọc là “không $x$”) cho phủ định của nó: $\lnot x$ đúng khi $x$ sai và ngược lại. Mỗi biến $x$ và phủ định $\lnot x$ của nó được gọi là các literal. Một mệnh đề là một điều kiện dạng $a \lor b$ (đọc là “$a$ hoặc $b$”), với $a$, $b$ là hai literal; mệnh đề được thỏa khi ít nhất một trong hai literal đúng.

Ví dụ với ba biến $x_1, x_2, x_3$ và ba mệnh đề

cách gán $x_1$ đúng, $x_2$ sai, $x_3$ đúng thỏa cả ba mệnh đề.

Cách dễ nghĩ ra nhất là thử hết $2^n$ cách gán, mỗi cách kiểm $m$ mệnh đề, tốn $O(2^n \cdot m)$. Với $n = 30$ đã cần hơn $10^9$ cách gán, nên chỉ dùng được khi $n$ rất nhỏ. Điểm đặc biệt của 2-SAT là mỗi mệnh đề chỉ có hai literal, và nhờ vậy có cách giải tuyến tính bằng đồ thị.

IIĐồ thị kéo theo

Mệnh đề $a \lor b$ có nghĩa là: nếu $a$ sai thì $b$ phải đúng, và nếu $b$ sai thì $a$ phải đúng. Viết bằng ký hiệu kéo theo $\Rightarrow$:

Ta dựng đồ thị kéo theo: mỗi literal là một đỉnh, nên có $2n$ đỉnh; mỗi mệnh đề $a \lor b$ thêm hai cung $\lnot a \to b$ và $\lnot b \to a$. Một cung $u \to v$ nghĩa là “nếu $u$ đúng thì $v$ đúng”. Đi theo một đường $u \to \dots \to v$, các câu “nếu… thì…” nối tiếp nhau, nên nếu $u$ đúng thì mọi literal trên đường, kể cả $v$, đều phải đúng.

Trong code, biến $x$ (đánh số từ $0$) có hai đỉnh: literal $x$ là đỉnh $2x$, literal $\lnot x$ là đỉnh $2x + 1$. Hai đỉnh này chỉ khác nhau ở bit cuối, nên phủ định của đỉnh $u$ là đỉnh $u \oplus 1$, viết trong C++ là u ^ 1. Hàm thêm một mệnh đề chỉ có hai dòng:

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

Độ phức tạp: $O(1)$ cho mỗi mệnh đề, cả đồ thị có $2n$ đỉnh và $2m$ cung.

Trong mô phỏng dưới đây, hàng trên là các literal $x_k$, hàng dưới là $\lnot x_k$. Mỗi bước thêm hai cung của một mệnh đề; bước cuối tô các thành phần liên thông mạnh và đọc ra cách gán, sẽ nói ở mục sau.

IIIKiểm tra có nghiệm và dựng cách gán

Nhắc lại từ bài 3.9: hai đỉnh liên thông mạnh khi mỗi đỉnh đi tới được đỉnh kia, và quan hệ này chia các đỉnh thành các thành phần liên thông mạnh.

Nếu $x$ và $\lnot x$ nằm trong cùng một thành phần liên thông mạnh, thì có đường từ $x$ tới $\lnot x$ và có đường từ $\lnot x$ tới $x$. Gán $x$ đúng thì $\lnot x$ phải đúng, tức $x$ sai; gán $x$ sai thì $\lnot x$ đúng, kéo theo $x$ đúng. Cả hai cách đều mâu thuẫn, nên các mệnh đề không có nghiệm. Điều bất ngờ là chiều ngược lại cũng đúng: nếu không biến nào nằm cùng thành phần với phủ định của nó, thì luôn có nghiệm, và dựng được ngay.

Thuật toán Kosaraju ở bài 3.9 đánh số các thành phần theo thứ tự tô pô: nếu có cung từ thành phần mang số $i$ tới thành phần mang số $j$ khác nó thì $i < j$. Cách gán là: với mỗi biến $x$, chọn literal nằm ở thành phần có số lớn hơn, tức là đứng sau trong thứ tự tô pô. Nghĩa là $x$ đúng khi số thành phần của $x$ lớn hơn số thành phần của $\lnot x$, và sai trong trường hợp ngược lại.

Mô phỏng dưới đây là một hệ không có nghiệm: $x_1$ kéo theo cả $x_3$ lẫn $\lnot x_3$, còn $\lnot x_1$ kéo theo cả $x_2$ lẫn $\lnot x_2$. Bạn có thể sửa một mệnh đề để hệ có nghiệm:

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

Đề. Có $m \le 10^5$ tùy chọn, mỗi tùy chọn bật hoặc tắt, và $n \le 10^5$ yêu cầu. Mỗi yêu cầu gồm hai điều kiện dạng + x (tùy chọn $x$ bật) hoặc - x (tùy chọn $x$ tắt), và cần ít nhất một trong hai điều kiện đúng. In + hoặc - cho từng tùy chọn, hoặc IMPOSSIBLE nếu không có cách nào.

Lời giải. Mỗi yêu cầu đúng là một mệnh đề $a \lor b$. Tùy chọn $x$ (đánh số từ $1$) bật là đỉnh $2(x - 1)$, tắt là đỉnh $2(x - 1) + 1$. Ta dựng đồ thị kéo theo cùng đồ thị ngược của nó, chạy Kosaraju như bài 3.9: lần duyệt thứ nhất ghi thứ tự xong, lần thứ hai duyệt đồ thị ngược theo thứ tự xong giảm dần và đánh số thành phần từ $1$. Sau đó kiểm từng biến, rồi đọc cách gán theo quy tắc ở trên. Đồ thị kéo theo có thể có hàng triệu cung, nên danh sách kề lưu kiểu int cho đỡ tốn bộ nhớ.

#include <bits/stdc++.h>
using namespace std;
#define ll long long
const ll N = 2e5 + 5;
ll n, m, k, vis[N], comp[N];
vector<int> g[N], rg[N], ord;

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

void dfs1(ll u) {
    vis[u] = 1;
    for (int v : g[u])
        if (!vis[v]) dfs1(v);
    ord.push_back(u);
}

void dfs2(ll u) {
    comp[u] = k;
    for (int v : rg[u])
        if (!comp[v]) dfs2(v);
}

signed main() {
    ios::sync_with_stdio(false);
    cin.tie(0);
    cin >> n >> m;
    for (ll i = 1; i <= n; i++) {
        char s1, s2;
        ll x1, x2;
        cin >> s1 >> x1 >> s2 >> x2;
        clause(2 * (x1 - 1) + (s1 == '-'), 2 * (x2 - 1) + (s2 == '-'));
    }
    for (ll u = 0; u < 2 * m; u++)
        if (!vis[u]) dfs1(u);
    for (ll i = 2 * m - 1; i >= 0; i--)
        if (!comp[ord[i]]) {
            k++;
            dfs2(ord[i]);
        }
    for (ll x = 0; x < m; x++)
        if (comp[2 * x] == comp[2 * x + 1]) {
            cout << "IMPOSSIBLE\n";
            return 0;
        }
    for (ll x = 0; x < m; x++) cout << (comp[2 * x] > comp[2 * x + 1] ? '+' : '-') << ' ';
    cout << '\n';
}

ChạyInput4 3
+ 1 + 1
- 2 - 2
+ 3 + 3
+ 1 - 2

Output+ - +

Độ phức tạp: $O(n + m)$, vì Kosaraju duyệt mỗi đỉnh và mỗi cung hai lần; với $n = m = 10^5$ cần khoảng $1{,}2 \cdot 10^6$ phép tính.

IVDịch các ràng buộc khác thành mệnh đề

Nhiều bài không cho sẵn mệnh đề, mà cho các ràng buộc giữa hai biến. Mỗi ràng buộc như vậy thường dịch được thành một hoặc hai mệnh đề:

• Ép $a$ đúng: mệnh đề $a \lor a$, cho cung $\lnot a \to a$ (nếu $a$ sai thì $a$ phải đúng).
• $a$ bằng $b$: hai mệnh đề $a \lor \lnot b$ và $\lnot a \lor b$.
• $a$ khác $b$: hai mệnh đề $a \lor b$ và $\lnot a \lor \lnot b$.
• Không được cùng đúng: mệnh đề $\lnot a \lor \lnot b$.

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

Đề. Có $N \le 1000$ biến nhận giá trị $0$ hoặc $1$ và $M \le 10^6$ ràng buộc dạng $X_a \ \mathrm{op}\ X_b = c$, với phép toán là AND, OR hoặc XOR và $c$ là $0$ hoặc $1$. Hỏi có cách gán thỏa mọi ràng buộc không.

Lời giải. Coi giá trị $1$ là đúng. Mỗi ràng buộc dịch thành một hoặc hai mệnh đề theo bảng trên:

• AND bằng $1$: ép cả hai đúng. AND bằng $0$: không được cùng đúng.
• OR bằng $1$: $a \lor b$. OR bằng $0$: ép cả hai sai.
• XOR bằng $1$: $a$ khác $b$. XOR bằng $0$: $a$ bằng $b$.

Sau đó dựng đồ thị kéo theo trên $2N$ đỉnh và kiểm như ví dụ trước. Mỗi ràng buộc cho tới hai mệnh đề, nên đồ thị có tới $4 \cdot 10^6$ cung, cộng thêm chừng ấy cung ở đồ thị ngược.

#include <bits/stdc++.h>
using namespace std;
#define ll long long
const ll N = 2005;
ll n, m, k, vis[N], comp[N];
vector<int> g[N], rg[N], ord;

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

void dfs1(ll u) {
    vis[u] = 1;
    for (int v : g[u])
        if (!vis[v]) dfs1(v);
    ord.push_back(u);
}

void dfs2(ll u) {
    comp[u] = k;
    for (int v : rg[u])
        if (!comp[v]) dfs2(v);
}

signed main() {
    ios::sync_with_stdio(false);
    cin.tie(0);
    cin >> n >> m;
    for (ll i = 0; i < m; i++) {
        ll a, b, c;
        string op;
        cin >> a >> b >> c >> op;
        ll 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);
        }
    }
    for (ll u = 0; u < 2 * n; u++)
        if (!vis[u]) dfs1(u);
    for (ll i = 2 * n - 1; i >= 0; i--)
        if (!comp[ord[i]]) {
            k++;
            dfs2(ord[i]);
        }
    bool ok = 1;
    for (ll x = 0; x < n; x++)
        if (comp[2 * x] == comp[2 * x + 1]) ok = 0;
    cout << (ok ? "YES" : "NO") << '\n';
}

ChạyInput3 3
0 1 1 XOR
1 2 1 AND
0 2 1 OR

OutputYES

Độ phức tạp: $O(N + M)$; với $M = 10^6$ cần khoảng $1{,}6 \cdot 10^7$ phép tính để dựng và duyệt cả hai đồ thị.

Với đồ thị có hàng triệu cung, cách lưu danh sách kề ảnh hưởng nhiều tới tốc độ:

Lưu các cung trong một mảng liền nhau (đếm bậc của từng đỉnh, cộng dồn để biết chỗ bắt đầu, rồi điền cung vào) nhanh hơn vector<int> g[N] khoảng $6$ lần, tính cả thời gian dựng đồ thị. Khi đọc được hết mệnh đề trước rồi mới chạy, và giới hạn thời gian chặt, nên cân nhắc cách lưu này.

Sử dụng kiến thức này cũng có thể giải bài có một biến nhận giá trị nguyên $f$ từ $1$ tới $K$, chẳng hạn mức công suất. Dùng $K$ literal “$f \ge k$” với $k = 1, 2, \dots, K$, nối thành chuỗi kéo theo “$f \ge k + 1$” $\Rightarrow$ “$f \ge k$”. Một điều kiện như “chọn trạm $i$ thì $l_i \le f \le r_i$” khi đó thành hai mệnh đề: chọn trạm $i$ kéo theo “$f \ge l_i$”, và chọn trạm $i$ kéo theo phủ định của “$f \ge r_i + 1$”.

VChọn một trong hai phương án có xung đột

Dạng hay gặp nhất của 2-SAT: mỗi đối tượng $i$ phải chọn đúng một trong hai phương án, phương án $0$ hoặc phương án $1$, và một số cặp phương án của hai đối tượng khác nhau xung đột, không được chọn cùng lúc. Ta dùng một biến cho mỗi đối tượng: literal “đối tượng $i$ chọn phương án $p$”. Với mỗi cặp xung đột “đối tượng $i$ chọn $p$” và “đối tượng $j$ chọn $q$”, thêm mệnh đề cấm: không ($i$ chọn $p$) hoặc không ($j$ chọn $q$). Duyệt mọi cặp đối tượng và mọi cặp phương án tạo ra $O(n^2)$ mệnh đề, đủ dùng khi $n$ cỡ vài nghìn.

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

Đề. Có $N \le 1000$ lá cờ, cờ thứ $i$ đặt ở tọa độ $X_i$ hoặc $Y_i$. Mọi cặp cờ phải cách nhau ít nhất $D$. In Yes cùng một cách đặt, hoặc in No nếu không đặt được.

Lời giải. Literal $2i + p$ nghĩa là “cờ $i$ đặt ở phương án $p$”, với phương án $0$ là $X_i$ và phương án $1$ là $Y_i$; literal $2i + 1$ đúng là phủ định của literal $2i$, đúng như cách đánh số ở trên. 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$, thêm mệnh đề cấm trên phủ định của cả hai lựa chọn. Có tới $4 \binom{N}{2} \approx 2 \cdot 10^6$ mệnh đề, rồi giải 2-SAT như các ví dụ trước; cờ $i$ đặt ở $X_i$ khi số thành phần của đỉnh $2i$ lớn hơn của đỉnh $2i + 1$.

#include <bits/stdc++.h>
using namespace std;
#define ll long long
const ll N = 2005;
ll n, d, k, vis[N], comp[N], pos[N][2];
vector<int> g[N], rg[N], ord;

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

void dfs1(ll u) {
    vis[u] = 1;
    for (int v : g[u])
        if (!vis[v]) dfs1(v);
    ord.push_back(u);
}

void dfs2(ll u) {
    comp[u] = k;
    for (int v : rg[u])
        if (!comp[v]) dfs2(v);
}

signed main() {
    ios::sync_with_stdio(false);
    cin.tie(0);
    cin >> n >> d;
    for (ll i = 0; i < n; i++) cin >> pos[i][0] >> pos[i][1];
    for (ll i = 0; i < n; i++)
        for (ll j = i + 1; j < n; j++)
            for (ll p = 0; p < 2; p++)
                for (ll q = 0; q < 2; q++)
                    if (llabs(pos[i][p] - pos[j][q]) < d) clause((2 * i + p) ^ 1, (2 * j + q) ^ 1);
    for (ll u = 0; u < 2 * n; u++)
        if (!vis[u]) dfs1(u);
    for (ll i = 2 * n - 1; i >= 0; i--)
        if (!comp[ord[i]]) {
            k++;
            dfs2(ord[i]);
        }
    for (ll i = 0; i < n; i++)
        if (comp[2 * i] == comp[2 * i + 1]) {
            cout << "No\n";
            return 0;
        }
    cout << "Yes\n";
    for (ll i = 0; i < n; i++) cout << (comp[2 * i] > comp[2 * i + 1] ? pos[i][0] : pos[i][1]) << '\n';
}

ChạyInput2 8
3 13
5 7

OutputYes
13
5

Độ phức tạp: $O(N^2)$ cho việc tạo mệnh đề và chạy Kosaraju; với $N = 1000$ cần khoảng $10^7$ phép tính.

Sử dụng kiến thức này cũng có thể giải bài: mỗi sự kiện chọn tổ chức nghi lễ ở đầu hoặc ở cuối khoảng thời gian của nó, và hai nghi lễ không được chồng lên nhau. Hai phương án xung đột khi hai khoảng thời gian giao nhau. Khi đề hỏi khoảng cách $D$ lớn nhất có thể (thay vì cho trước $D$), ta chặt nhị phân trên $D$ (bài 0.6) và mỗi bước kiểm bằng 2-SAT.