下文中以 ⟨⟩\langle\rangle 表示矛盾的集合，[][] 表示题目给定的的集合

定义

2-SAT，简单的说就是给出 nn 个集合，每个集合有两个元素，已知若干个 ⟨a,b⟩\langle a,b \rangle ，表示 aa 与 bb 矛盾（其中 aa 与 bb 属于不同的集合）。然后从每个集合选择一个元素，判断能否一共选 nn 个两两不矛盾的元素。显然可能有多种选择方案，一般题中只需要求出一种即可。
——来自oiwiki

解法

对于 2-sat 问题，我们可以将它抽象成一个图论问题，建图来完成。

建图

首先考虑如何建图，对于两个集合内 [a,b][a,b]， [c,d][c,d]，若 a,ca, c 矛盾，则选 aa 就只能选 dd，选 cc 就只能选 bb。以此为基础，则可以连接 a→da \rightarrow d， c→bc \rightarrow b 两条有向边，对于 P4782 【模板】2-SAT 中的四种条件，我们可以以以下方式建边:

  1. a, b, true, true
    a1→b0a_1 \rightarrow b_0，b1→a0b_1 \rightarrow a_0
  2. a, b, false, false
    a0→b1a_0 \rightarrow b_1，b0→a1b_0 \rightarrow a_1
  3. a, b, true, false
    a1→b1a_1 \rightarrow b_1，b0→a0b_0 \rightarrow a_0
  4. a, b, false, true
    a0→b0a_0 \rightarrow b_0，b1→a1b_1 \rightarrow a_1

对于这样建完的图，就可以接着进行处理了。

求解

判负

对于这个图，我们可以发现，如果一个集合 [a,b][a,b]，两个点在同一个强连通分量里，显然是不成立的。（显然一个强连通分量里一旦选就要全选）

那么可以使用 tarjan 算法来求解强连通分量，但是还有一个问题，如何求一个字典序最小的可行解？

求可行解

如果有这样一个图（aa，bb 在同一集合里）：

那么显然只能选 aa，反过来？显然只能选 bb.

如果没有连边呢？选 aa 的字典序一定最小。

可以发现一个共同点，两个点间，选拓扑序较大的一个是可以满足字典序最小的可行解的，至于拓扑序，tarjan 中缩出的点的编号便是拓扑序的逆序。

所以问题就解决了：按 tarjan 的 color 优先选 color 更小的。

完结～～

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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
//problem: P4782 【模板】2-SAT 
//data: 2023.10.16-16:15
#include <bits/stdc++.h>
#define int long long
#define FH signed
using namespace std;

const int N = 2e6 + 10;

vector<int> e[N];
int n, m;

stack<int> st;
bool vis[N];
int dfn[N], low[N], idx;
int color[N], bl;
void tarjan(int u)
{
    dfn[u] = low[u] = ++ idx;
    vis[u] = 1;
    st.push(u);
    for(auto v : e[u])
    {
        if(!dfn[v])
        {
            tarjan(v);
            low[u] = min(low[u], low[v]);
        }
        else if(vis[v]) low[u] = min(low[u], dfn[v]);
    }
    if(dfn[u] == low[u])
    {
        int z;
        ++ bl;
        do
        {
            z = st.top();
            st.pop();
            vis[z] = 0;
            color[z] = bl;
        } while(z != u);
    }
}

void add(int a, int b, int opt)
{
    if(opt == 1) // x == y == 0
    {
        e[a + n].push_back(b);
        e[b + n].push_back(a);  
    }
    else if(opt == 2) //x == y == 1
    {
        e[a].push_back(b + n);
        e[b].push_back(a + n);
    }
    else if(opt == 3) //x == 1, y == 0
    {
        e[a].push_back(b);
        e[b + n].push_back(a + n);
    }
    else //x == 0, y == 1
    {
        e[a + n].push_back(b + n);
        e[b].push_back(a);
    }
}

void two_sat()
{
    cin >> n >> m;
    for(int i = 1; i <= m; i ++)
    {
        int a, b;
        bool x, y;
        cin >> a >> x >> b >> y;
        if(x == y && y == 0) add(a, b, 1);
        if(x == y && y == 1) add(a, b, 2);
        if(x == 1 && y == 0) add(a, b, 3);
        if(x == 0 && y == 1) add(a, b, 4);
    }
    for(int i = 1; i <= 2 * n; i ++)
        if(!dfn[i])
            tarjan(i);
    for(int i = 1; i <= n; i ++)
        if(color[i] == color[i + n])
        {
            cout << "IMPOSSIBLE\n";
            return ;
        }
    cout << "POSSIBLE\n";
    for(int i = 1; i <= n; i ++)
        if(color[i] < color[i + n]) cout << 0 << " ";
        else cout << 1 << " ";
}

FH main()
{
    two_sat();
  
    return 0;
}