差分约束系统与 2-SAT

将两者放在一起的原因是两者本质十分相像：

• 差分约束用于解多个二元不等式，其中要求变量为实数，不等式表示两个变量之差。
• 2-SAT 则用来解决布尔类型方程，每个方程同样只涉及两个变量。

差分约束系统

以模板题 P5960 【模板】差分约束 - 洛谷 为例，差分约束本质上是由多个形如：

$$\begin{cases} x_{c_1}-x_{c'_1}\leq y_1 \\x_{c_2}-x_{c'_2} \leq y_2 \\ \cdots\\ x_{c_m} - x_{c'_m}\leq y_m\end{cases}$$

组成的不等式组，对这个不等式进行求解或判断是否无解（或无穷解）。

问题转化

既然知道差分约束与最短路有关，我们考虑转化问题，我们在不等式组中单独拎出一个式子：

$$x_i - x_j \le k$$

钦定 $x_i$ 为要更新的变量，将其他元素移到不等式右侧，得到：

$$x_i \le x_j + k$$

如果我们将 $x_i$ 表示为图论上的点 $i$ 到达一个源点的最短距离的话，这就转化成了最短路问题：

$$dist_i \le dist_j + k$$

这个式子的几何含义是 从源点到 $i$ 点的最短距离不会大于源点到 $j$ 点的最短距离加上 $k$，不等式的等号成立当源点到 $i$ 点的最短路径经过 $j$ 点和一条边权为 $k$ 的边，这个问题：

$$dist_i \le dist_j + k \iff \exist \ edge(j, i, k)$$

其他类似的不等式子也是类似的转化，包括但不限于：

$$x_i = x_j \iff x_i \le x_j \wedge x_j \le x_i \iff \exist \ edge(i, j, 0) \wedge edge(j, i, 0) \\ x_i - x_j \ge k \iff x_j \le x_i - k \iff \exist \ edge(i, j, -k)$$

如果存在 $\gt$ 或者 $\lt$ 的情况，在相应的一边加上 $1$ 即可转化为 $\le$ 和 $\ge$ 的式子。

图上处理

上文我们将所有的不等式组转化为了有 $\le$ 的式子，这样子所求的系统只能适用于最短路模型，如果我们要求出最长路，只需要在转化时为 $\ge$ 的式子，并将边权转化即可。

最短路求所有 $x$ 的最大解，最长路求所有 $x$ 的最小解。

看似十分的反直觉，但是我们根据定义可知，只有当整张图松弛完毕时，此时的系统才是合法的，所求的最短路模型刚好是合法方案中最大的一个（所有的边此时都满足了边界条件），最长路模型亦然。

无穷解我们不做探讨（即使有我们也只要求出最值即可）。

至于无解的情况，就是变量自身存在类似：

$$x_i \le x_i + k (k \lt 0)$$

的自相矛盾的行为，换句话说，变量自己被自己所松弛了，而这个边权是个负数，在图上模型就被当做是存在了负环。因此判断无解十分方便，只需要用 SPFA 算法判断负环即可。

代码示范

SPFA 算法判断负环：

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

bool spfa(int st)
{
    memset(dist, 0x3f, sizeof dist), memset(vis, 0, sizeof vis);
    // 最短路时需要初始化，最长路没有必要
    hh = 0, tt = -1, que[++ tt] = st;
    dist[st] = 0, vis[st] = true;

    while (hh <= tt)
    {
        int ver = que[hh ++];
        vis[ver] = false;

        for (int i = h[ver]; ~i; i = ne[i])
        {
            int to = e[i];
            if (dist[to] > dist[ver] + w[i])
            {
                dist[to] = dist[ver] + w[i];
                if (!vis[to])
                {
                    if (++ cnt[to] > n) return false;    // 还有一个超级源点
                    vis[to] = true, que[++ tt] = to;
                }
            }
        }
    }
    return true;
}

2-SAT

K-SAT 问题，又称作 K - 适定性（Satisfiability）问题，是一系列布尔类型方程组问题，当 $k \gt 2$ 时，此类问题被证明是 NP 完全的，因此我们只讨论 $k = 2$ 的情况，

2-SAT，简单来说就是给定 $n$ 个集合，每个集合是一个二元组 $\left \langle a, b \right \rangle$​，从每个集合中选出一个元素，保证不会与别的选取元素发生冲突，判断是否有解并输出有解的方案（通常只需要一种）。

问题转化

形式化的，我们将一个布尔变量分为两种状态：true 和 false，显然一个变量不可能同时有两种状态，与 2-SAT 问题中二元组只能选取其中之一的要求类似，因此问题得以转化。

像例题 P4782 【模板】2-SAT - 洛谷 所述：

有 $n$ 个布尔变量 $x_1$$\sim$$x_n$，另有 $m$ 个需要满足的条件，每个条件的形式都是 「$x_i$ 为 true / false 或 $x_j$ 为 true / false」。比如 「$x_1$ 为真或 $x_3$ 为假」、「$x_7$ 为假或 $x_2$ 为假」。

我们定义一张图，边 $a\to b$ 表示节点 $a$ 的变量取值一旦成立，那么节点 $b$ 的取值也必须成立，就这样一旦改变一个值，其他有关联的值都会相应改变。不难发现，如果一些点位于一个强连通分量之内，说明它们应当自洽，当且仅当一个变量的两个状态都在一个强连通分量之内，2-SAT 不成立，即无解。

建图方式

接下来分类讨论二元组 $\left \langle a, b \right \rangle$ 不同取值的连边方案（此处的二元组是不同变量之间的关系）：

1. $\left \langle a \vee b \right \rangle$：即 $a$ 或 $b$ 成立，也就是说 $a$ 或 $b$ 不成立时，另一个必然成立，建图如下：

$$\neg a \to b \wedge \neg b \to a$$

2. $\left \langle a \wedge b \right \rangle$：两者必须同时成立，如下：

$$a \to b \wedge b \to a \wedge \neg a \to \neg b \wedge \neg b \to \neg a$$

3. 变量取特定值时，若规定 $a = true$，连边如下：

$$\neg a \to a$$

实际运用场景中，可能会出现 $[a = true] = false$ 的场景，此时调换 $a$ 与 $\neg a$ 即可。

输出方案

有向图中寻找强连通分量可以使用 Tarjan，使用之后遍历所有点判断是否无解即可：

1
2

for (int ver = 1; ver <= n; ver ++)
    if (id[ver] == id[ver + n]) return puts("IMPOSSIBLE"), 0;

如果有解的话，我们将 Tarjan 缩点后的 topo 图从后往前遍历，每次找到出度为 $0$ 的点，第一次钦定这个缩点为 $1$，说明这个 SCC 中所有点都被选取了，依据逆拓扑序，剩下的点都可以被选出来（之所以逆拓扑是因为不会有后效性问题）。

巧的是 Tarjan 缩点后的每个点所属 SCC 编号从小到大刚好是逆拓扑序的，我们只需要从小到大判断 $a_i$ 还是 $\neg a_i$ 先被定下即可，这就构成了一种方案。

1
2
3

for (int ver = 1; ver <= n; ver ++)
        cout << (id[ver] < id[ver + n]) << ' ';
cout << '\n';

代码示范

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

#include <bits/stdc++.h>

using namespace std;

// #define int long long
#define DEBUG(a) cerr << #a << " = " << a << '\n'
#define x first
#define y second
#define File(a) freopen(a".in", "r", stdin), freopen(a".out", "w", stdout)

typedef long long LL;
typedef pair<int, int> PII;

const int N = 2000010, M = N << 1;    // 开两倍空间（点集为两倍）
const int INF = 0x3f3f3f3f;

int n, m;
int h[N], e[M], ne[M], w[M], idx;
int dfn[N], low[N], timestamp;
int stk[N], top;
bool in_stk[N];
int scc_cnt, id[N];

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

void tarjan(int ver)
{
    dfn[ver] = low[ver] = ++ timestamp;
    stk[++ top] = ver, in_stk[ver] = true;
    for (int i = h[ver]; ~i; i = ne[i])
    {
        int to = e[i];
        if (!dfn[to])
        {
            tarjan(to);
            low[ver] = min(low[ver], low[to]);
        }
        else if (in_stk[to])
            low[ver] = min(low[ver], dfn[to]);
    }
    if (low[ver] == dfn[ver])
    {
        ++ scc_cnt;
        int temp;
        do {
            temp = stk[top --], in_stk[temp] = false;
            id[temp] = scc_cnt;
        } while (temp != ver);
    }
}

signed main()
{
    // ios::sync_with_stdio(0), cin.tie(0), cout.tie(0);
    memset(h, -1, sizeof h);
    cin >> n >> m;
    while (m --)
    {    // 这里都是 a 或 b 的情况，但是变量可以取假的
        int a, b, tpa, tpb; cin >> a >> tpa >> b >> tpb;
        if (tpa && tpb) // a == 1 && b == 1
            add(a + n, b), add(b + n, a);
        else if (tpa && !tpb)
            add(a + n, b + n), add(b, a);
        else if (!tpa && tpb)
            add(a, b), add(b + n, a + n);
        else add(a, b + n), add(b, a + n);
    }

    for (int ver = 1; ver <= n << 1; ver ++)// 注意边界
        if (!dfn[ver]) tarjan(ver);

    for (int ver = 1; ver <= n; ver ++)
        if (id[ver] == id[ver + n]) return puts("IMPOSSIBLE"), 0;
    puts("POSSIBLE");
    for (int ver = 1; ver <= n; ver ++)
        cout << (id[ver] < id[ver + n]) << ' ';
    cout << '\n';

    return 0;
}

References

P4782 【模板】2-SAT - 洛谷 | 计算机科学教育新生态 (luogu.com.cn)

2-SAT - OI Wiki (oi-wiki.org)