2-SAT

2-SAT

给 $n$ 个命题，每个命题只有两个变量，每个变量要么是 $1$(真) 要么是 $0$(假)。

询问是否有合法的构造使得所有的命题的与成立。

1. $a\to b⟺\neg a\vee b$ ($\to$ 是蕴含，若 p 则 q的意思)
2. $a\to b⟺\neg b\to \neg a$ (原命题和逆否命题等价)
3. $x$ 和 $\neg x$ 在同一个 SCC 中 无解。（3是有解的必要条件）
4. 若上述条件成立，一定有解吗？（证明充分性）
   1. 答案：一定有。
   2. 发现，如果有 $a\to x_1\to x_2\to ...\to b$ , $b\to y_1\to y_2\to ...\to a$ 。那么根据逆否命题一定有：$\neg a\leftarrow x_1\leftarrow x_2\leftarrow ...\leftarrow \neg b$ , $\neg b\leftarrow y_1\leftarrow y_2\leftarrow ...\leftarrow \neg a$ 。所以如果 $a,b$ 在同一个 SCC 中，$\neg a,\neg b$ 一定也在同一个 SCC 中。
   3. 每个 SCC 中的变量要么都选，要么都不选。每个SCC一定有一个和他对偶的SCC。
   4. 构造方式：先 tarjan 缩点，进行拓扑排序，对于一个变量的两种情况，取更靠后的那一种。

---

命题条件总结：

1. $a\vee b⟺\neg a\to b⟺\neg b\to a$
2. $a\to b⟺\neg a\vee b⟺\neg b\vee a$
3. $a=1⟺a\vee a$
4. $a=0⟺\neg a\vee \neg a$

---

连边的方式：

1. i 对应 i+n , 在模板题中有：

while (m -- )
{
    int i, a, j, b;
    scanf("%d%d%d%d", &i, &a, &j, &b);
    // i,i+n ; j,j+n
    add(i + n * (a & 1), j + n * (b ^ 1));
    add(j + n * (b & 1), i + n * (a ^ 1));
}
1
2
3
4
5
6
7
8

2. 2 * i 为真，2 * i + 1是假

add(2 * i + !a, 2 * j + b);
add(2 * j + !b, 2 * i + a);
1
2

---

因为tarjan得到的id是拓扑逆序，最后正序遍历就行了。

#include 
#include 
#include 
#include 

using namespace std;

const int N = 2000010, M = 2000010;

int n, m;
int h[N], e[M], ne[M], idx;
int dfn[N], low[N], ts, stk[N], top;
int id[N], cnt;
bool ins[N];

void add(int a, int b)
{
    e[idx] = b, ne[idx] = h[a], h[a] = idx ++ ;
}

void tarjan(int u)
{
    dfn[u] = low[u] = ++ ts;
    stk[ ++ top] = u, ins[u] = true;
    for (int i = h[u]; ~i; i = ne[i])
    {
        int j = e[i];
        if (!dfn[j])
        {
            tarjan(j);
            low[u] = min(low[u], low[j]);
        } else if (ins[j]) low[u] = min(low[u], dfn[j]);
    }

    if (low[u] == dfn[u])
    {
        int y;
        cnt ++ ;
        do
        {
            y = stk[top -- ], ins[y] = false, id[y] = cnt;
        } while (y != u);
    }
}

int main()
{
    scanf("%d%d", &n, &m);
    memset(h, -1, sizeof h);

    while (m -- )
    {
        int i, a, j, b;
        scanf("%d%d%d%d", &i, &a, &j, &b);
        // i,i+n ; j,j+n
        add(i + n * (a & 1), j + n * (b ^ 1));
        add(j + n * (b & 1), i + n * (a ^ 1));
    }

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

    for (int i = 1; i <= n; i ++ )
        if (id[i] == id[i + n])
        {
            puts("IMPOSSIBLE");
            return 0;
        }

    puts("POSSIBLE");
    for (int i = 1; i <= n; i ++ )
        if (id[i] < id[i + n]) printf("1 ");
        else printf("0 ");

    return 0;
}
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
74
75
76
77