2-SAT 笔记

发表于2021-07-27更新于2023-09-15字数统计2.5k阅读时长25分

SAT 是适定性问题 (Satisfiability) 问题的简称。一般形式为 kk - 适定性问题，简称 k-SAT。而当 k>2k > 2 时该问题为 NP 完全的。所以我们只研究 k=2k = 2 的情况。

定义

2-SAT 简单地讲就是给出 nn 个集合，每个集合有两个元素 <a,b><a, b>，以及若干个矛盾关系 (如 aia_i 与 bib_i 或 bjb_j不能同时选择)。然后从每个集合选择 aa 或 bb，判断能否使这些元素两两不矛盾。

Solution

将矛盾关系转化为形如 (xi∨xj)∧(¬xp∨xq)∧...(x_i \vee x_j) \wedge (\neg x_p \vee x_q) \wedge ... 的合取式，最后要使得该逻辑表达式的值为 1。

对于每组 (i∨j)(i \vee j)，其等值于 ¬i→j\neg i \rightarrow j 以及 ¬j→i\neg j \rightarrow i。表示 i,ji, j 至少选择一个，如果不选 ii，则必须选 jj；不选 jj 则必须选 ii。否则合取式的值为 0。

例如 ai和bja_i 和 b_j 存在矛盾，则可得 ai→¬bja_i \rightarrow \neg b_j 以及 bj→¬aib_j \rightarrow \neg a_i，也等值于 ¬ai∨¬bj\neg a_i \vee \neg b_j，表示 aia_i 和 bjb_j 至少有一个不选。

据此可建立 2n2n 个点的有向图。对于每个变量 xix_i，用节点 ii 表示 xix_i 为真，用节点 i+ni + n 或 i⊕1i \oplus 1 表示 xix_i 为假。如果 i→ji \rightarrow j，则从 ii 向 jj 连一条有向边 (ii，jj 可能带 ¬\neg 符号)。

对于每个变量 xx 有 4 种情况：

  • xx 与 ¬x\neg x 无关系，取值任意
  • x→¬xx \rightarrow \neg x，取 xx 为假，否则蕴含式的值为假
  • ¬x→x\neg x \rightarrow x，取 xx 为真
  • x→¬xx \rightarrow \neg x 并且 ¬x→x\neg x \rightarrow x，无解

对于上述第四种情况，根据假言三段论可知，xx 和 ¬x\neg x 一定在同一个联通分量中。于是跑一遍 tarjantarjan，判断 ii 与 i+ni + n 是否在同一个强连通分量中。

tarjan 模板
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
int n, m, tot, top, cntscc;
vector<int> g[MAXN * 2];
int dfn[MAXN * 2], low[MAXN * 2], stk[MAXN * 2], ins[MAXN * 2], belong[MAXN * 2];

void tarjan(int cur) {
    dfn[cur] = low[cur] = ++tot;
    stk[++top] = cur, ins[cur] = true;
    for (const auto& to : g[cur]) {
        if (!dfn[to]) {
            tarjan(to);
            low[cur] = min(low[cur], low[to]);
        } else if (ins[to]) {
            low[cur] = min(low[cur], dfn[to]);
        }
    }
    if (dfn[cur] == low[cur]) {
        ++cntscc;
        int tmp;
        do {
            tmp = stk[top--];
            ins[tmp] = false;
            belong[tmp] = cntscc;
        } while (cur != tmp);
    }
}

for (int i = 1; i <= 2 * n; i++) 
        if (!dfn[i]) tarjan(i);

可行解

任意解

模板题
因为 tarjantarjan 求强连通分量时使用了栈，所以 tarjantarjan 求得的 sccscc 编号相当于反拓扑序。所以如果 ii 所在的 sccscc 编号小于 i+ni + n 或 i⊕1i \oplus 1 所在的 sccscc 编号，则说明 ¬xi→∗xi\neg x_i \rightarrow ^* x_i，xi=truex_i = true。

时间复杂度 O(n+m)O(n + m)。

1
2
3
4
5
6
7
8
for (int i = 1; i <= n; i++)
    if (belong[i] == belong[i + n]) {
        cout << "IMPOSSIBLE" << "\n";
        return 0;
    }
cout << "POSSIBLE" << "\n";
for (int i = 1; i <= n; i++) // !x -> x thus x = ture in rev topo order
    ans[i] = belong[i] < belong[i + n], cout << ans[i] << " ";

最小字典序解

注意多组数据
如果需要求出被选择的元素的最小字典序，这时候就不能使用 tarjantarjan 了。

考虑从小到大枚举元素，优先使用 dfs 将该元素 xx 对应节点以及之后的节点染色为 truetrue，如果出现矛盾则将 ¬x\neg x 对应的节点以及之后的节点染色为 truetrue。如果都不行，则无解。

可以通过栈或 vector 来撤销之前的染色操作。

时间复杂度 O(nm)O(nm)。

O(nm)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
#include <bits/stdc++.h>

using namespace std;

#define boost ios::sync_with_stdio(false), cin.tie(0), cout.tie(0);

constexpr int MAXN = 8008, MOD = 1e9 + 7;

int n, m, top;
vector<int> g[MAXN * 2];
array<int, MAXN * 2> mark, stk;

void add(int u, int v) { g[u].emplace_back(v); }

void init() {
    for (int i = 0; i < 2 * n; i++) g[i].clear();
    fill(mark.begin(), mark.end(), 0);
}

bool dfs(int cur) { // 将 current 标记为 true
    if (mark[cur ^ 1]) return false;
    if (mark[cur]) return true;
    mark[cur] = true;
    stk[top++] = cur;
    for (auto& to : g[cur]) if (!dfs(to)) return false;
    return true;
}

bool solve() {
    for (int i = 0; i < 2 * n; i += 2) {
        if (!mark[i] && !mark[i ^ 1]) {
            top = 0;
            if (!dfs(i)) {
                while (top > 0) mark[stk[--top]] = false;
                if (!dfs(i + 1)) return false;
            }
        }
    }
    return true;
}

int main() {
    boost;
    while (cin >> n >> m) {
        init();
        for (int i = 1, a, b; i <= m; i++) {
            cin >> a >> b;
            a--, b--;
            add(a, b ^ 1);  // !a | !b
            add(b, a ^ 1);
        }
        if (!solve()) {
            cout << "NIE\n";
        } else {
            for (int i = 0; i < 2 * n; i++)
                if (mark[i]) cout << i + 1 << "\n";
        }
    }
    return 0;
}

参考链接

2-SAT
OI-wiki

例题

Kuta Puzzle

题目链接
xix_i 取值为 1 对应节点 ii，否则对应 i+ni + n。

分 6 种情况讨论:

  • xa∧xb=0x_a \wedge x_b = 0
    对应的逻辑表达式为 ¬xa∨¬xb\neg x_a \vee \neg x_b，等值于 xa→¬xbx_a \rightarrow \neg x_b 以及 xb→¬xax_b \rightarrow \neg x_a
  • xa∧xb=1x_a \wedge x_b = 1
    对应的逻辑表达式为 (xa∨xa)∧(xb∨xb)(x_a \vee x_a) \wedge (x_b \vee x_b)，等值于 (¬xa→xa)∧(¬xb→xb)(\neg x_a \rightarrow x_a) \wedge (\neg x_b \rightarrow x_b)
  • xa∨xb=0x_a \vee x_b = 0
    对应的逻辑表达式为 (¬xa∨¬xa)∧(¬xb∨¬xb)(\neg x_a \vee \neg x_a) \wedge (\neg x_b \vee \neg x_b)，等值于 (xa→¬xa)∧(xb→¬xb)(x_a \rightarrow \neg x_a) \wedge (x_b \rightarrow \neg x_b)
  • xa∨xb=1x_a \vee x_b = 1
    对应的逻辑表达式 (xa∨xb)(x_a \vee x_b)，等值于 (¬xa→xb)∧(¬xb→xa)(\neg x_a \rightarrow x_b) \wedge (\neg x_b \rightarrow x_a)
  • xa⊕xb=0x_a \oplus x_b = 0
    对应的逻辑表达式为 (xa∧xb)∨(¬xa∧¬xb)(x_a \wedge x_b) \vee (\neg x_a \wedge \neg x_b)。但我们需要的是合取式，所以需要等值演算一下，得到 (¬xa∨xb)∧(¬xb∨xa)(\neg x_a \vee x_b) \wedge (\neg x_b \vee x_a)。(其实异或为 0 也相当于 (xa↔xb)(x_a \leftrightarrow x_b))。
  • xa⊕xb=0x_a \oplus x_b = 0
    对应的逻辑表达式为 (xa↔¬xb)(x_a \leftrightarrow \neg x_b)，等值于 (¬xa∨¬xb)∧(xa∨xb)(\neg x_a \vee \neg x_b) \wedge (x_a \vee x_b)。

按照上述表达式建边即可。

Kuta Puzzle
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
#include <bits/stdc++.h>

using namespace std;

#define boost ios::sync_with_stdio(false), cin.tie(0), cout.tie(0);

constexpr int MAXN = 1e3 + 3, MOD = 1e9 + 7;

int n, m, tot, top, cntscc;
vector<int> g[MAXN * 2];
int dfn[MAXN * 2], low[MAXN * 2], stk[MAXN * 2], ins[MAXN * 2], belong[MAXN * 2], ans[MAXN];

void add(int u, int v) { g[u].emplace_back(v); }

void tarjan(int cur) {
    dfn[cur] = low[cur] = ++tot;
    stk[++top] = cur, ins[cur] = true;
    for (const auto& to : g[cur]) {
        if (!dfn[to]) {
            tarjan(to);
            low[cur] = min(low[cur], low[to]);
        } else if (ins[to]) {
            low[cur] = min(low[cur], dfn[to]);
        }
    }
    if (dfn[cur] == low[cur]) {
        ++cntscc;
        int tmp;
        do {
            tmp = stk[top--];
            ins[tmp] = false;
            belong[tmp] = cntscc;
        } while (cur != tmp);
    }
}


int main() {
    boost;
    cin >> n >> m;
    string type;
    for (int t = 1; t <= m; t++) {
        int a, b, c;
        cin >> a >> b >> c >> type;
        a++, b++;
        if (type == "AND") {
            if (c == 0) add(a, b + n), add(b, a + n);
            else add(a + n, a), add(b + n, b);
        } else if (type == "OR") {
            if (c == 0) add(a, a + n), add(b, b + n);
            else add(a + n, b), add(b + n, a);
        } else {
            if (c == 0) add(a, b), add(b, a), add(a + n, b + n), add(b + n, a + n);
            else add(a, b + n), add(b, a + n), add(b + n, a), add(a + n, b);
        }
    }
    for (int i = 1; i <= 2 * n; i++) 
        if (!dfn[i]) tarjan(i);
    for (int i = 1; i <= n; i++)
        if (belong[i] == belong[i + n]) {
            cout << "NO" << "\n";
            return 0;
        }
    cout << "YES" << "\n";
    return 0;
}

TV Show Game K

题目链接
题目大意是说每个人从 k≥3k \ge 3 盏灯 （灯的初始颜色未知）中选了 3 盏灯猜测颜色（红色或蓝色）。每个人都猜中 ≥2\ge 2 盏灯颜色即可满足。若可满足，则要求给出一种灯的颜色方案。

对于一组赋值: a x b y c z 来说：

  • 若 ¬a\neg a，则 b∧cb \wedge c
  • 若 ¬b\neg b，则 a∧ca \wedge c
  • 若 ¬c\neg c，则 a∧ba \wedge b

根据上述可得若干蕴含式，转化为 2-SAT 标准形式即可。

TV Show Game K
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
#include <bits/stdc++.h>

using namespace std;

#define boost ios::sync_with_stdio(false), cin.tie(0), cout.tie(0);

constexpr int MAXN = 1e4 + 4, MOD = 1e9 + 7;

int n, m, tot, top, cntscc;
vector<int> g[MAXN * 2];
int dfn[MAXN * 2], low[MAXN * 2], stk[MAXN * 2], ins[MAXN * 2], belong[MAXN * 2];
char ans[MAXN];

void add(int u, int v) { g[u].emplace_back(v); }

void tarjan(int cur) {
    dfn[cur] = low[cur] = ++tot;
    stk[++top] = cur, ins[cur] = true;
    for (const auto& to : g[cur]) {
        if (!dfn[to]) {
            tarjan(to);
            low[cur] = min(low[cur], low[to]);
        } else if (ins[to]) {
            low[cur] = min(low[cur], dfn[to]);
        }
    }
    if (dfn[cur] == low[cur]) {
        ++cntscc;
        int tmp;
        do {
            tmp = stk[top--];
            ins[tmp] = false;
            belong[tmp] = cntscc;
        } while (cur != tmp);
    }
}


int main() {
    boost;
    cin >> n >> m;
    string c[3];
    int l[3], p[3];
    for (int t = 1; t <= m; t++) { // 一个人猜 3 盏灯 a b c颜色 0/1，猜对至少 2 个则可满足
        for (int i = 0; i < 3; i++)
            cin >> l[i] >> c[i], p[i] = c[i] == "R" ? 1 : 0;

        add(l[0] + (1 - !p[0]) * n, l[1] + (1 - p[1]) * n);
        add(l[1] + (1 - !p[1]) * n, l[0] + (1 - p[0]) * n);
        add(l[0] + (1 - !p[0]) * n, l[2] + (1 - p[2]) * n);
        add(l[2] + (1 - !p[2]) * n, l[0] + (1 - p[0]) * n);

        add(l[1] + (1 - !p[1]) * n, l[0] + (1 - p[0]) * n);
        add(l[0] + (1 - !p[0]) * n, l[1] + (1 - p[1]) * n);
        add(l[1] + (1 - !p[1]) * n, l[2] + (1 - p[2]) * n);
        add(l[2] + (1 - !p[2]) * n, l[1] + (1 - p[1]) * n);

        add(l[2] + (1 - !p[2]) * n, l[0] + (1 - p[0]) * n);
        add(l[0] + (1 - !p[0]) * n, l[2] + (1 - p[2]) * n);
        add(l[2] + (1 - !p[2]) * n, l[1] + (1 - p[1]) * n);
        add(l[1] + (1 - !p[1]) * n, l[2] + (1 - p[2]) * n);
    }
    for (int i = 1; i <= 2 * n; i++) 
        if (!dfn[i]) tarjan(i);
    for (int i = 1; i <= n; i++)
        if (belong[i] == belong[i + n]) {
            cout << -1 << "\n";
            return 0;
        }
    for (int i = 1; i <= n; i++)
        ans[i] = belong[i] < belong[i + n] ? 'R' : 'B', cout << ans[i];
    return 0;
}

Coprime solitaire

链接