2-SAT

2-SAT 问题的定义

SAT：satisfiability，可满足性

2-SAT 是说约束条件在两两元素之间

一个比较典型的 2-sat 问题是聚会问题，每家夫妻二人必须去一个，给定一组关系，某两人关系不好不能同时出席，作为主办方能否请恰好 n 个人列席

思路

这种关系可以用图来表示

如 A 夫与 B 夫不和，那么选 A 夫只能选 B 妻，选 B 夫只能选 A 妻

这样就形成了两条有向边 (a1, b2) 和 (b1, a2)

几个概念：

1. 连通：有向图 G 中从点 A 可以走到点 B，B 也能走到点 A，称 A 与 B 是连通的
2. 强连通：有向图 G 中任意两个结点连通。
3. 强连通分量（Strongly Connected Components，SCC）：极大强连通子图

那么 2-SAT 问题就转化成了求特定规模的 SCC，或多个不冲突的 SCC 规模相加为特定值

Tarjan

Tarjan 算法可以求 SCC，具体如下：

考虑一个 dfs 生成树，其中出现的边分为 4 种：

1. 树枝边访问一个新的结点时形成的边
2. 返祖边当前结点的下一个结点是其祖先
3. 横叉边下一个结点已访问，但是不是祖先
4. 前向边下一个结点是子树里的结点

Tarjan 算法基于 dfs，SCC 必然是 dfs 搜索树中的一棵子树，这棵子树是有环的

在这棵子树中，“根结点”则是最早被 dfs 搜索到的、最早进栈的结点，那么，找到这个结点就等于找到了 SCC

当然，不是所有的子树都是 SCC，恰好 u 的子树中有一条返祖边指向 u 的情况，才会成环，才有 SCC

1. 进行一次 dfs，形成一个 dfs 生成树，用一个数组dfn[u]来表示遍历到点 u 的次序
2. low[u]表示以 u 为树根的树中，最早进栈的结点

u 的子树组成 SCC 的充要条件是：dfn[u] == low[u]

原因如下：在 u 之后进入栈的它的子树的结点，如果存在与 u 的返祖边，那么 u 就成了该子结点 v 的子结点，该子结点的 low[v] 就成了 low[u]了，在这种纠缠不清的情况中，能满足 dfn[u] == low[u] 的结点是唯一的，是先到先得的，也就是最早进入栈的子树根节点

low[u] = min
{
    dfn[u],
    low[v], (u,v)为树枝边
    dfn[v], (u,v)为返祖边/前向边
}
1
2
3
4
5
6

TARJAN_SEARCH(int u)
    vis[u] = true
    low[u] = dfn[u] = ++dfncnt
    把 u push 到栈内
    for each 与 u 连通的点 v
        if !vis[v]
            TARJAN_SEARCH(v) // 继续向下找
            low[u] = min(low[u], low[v])
        else if vis[v] && v 在栈里
            low[u] = min(low[u], dfn[v])
    if dfn[u] == low[u]
        // u 及其子树构成一个 SCC
        栈 pop，pop 出来的是 SCC 中一个顶点，直到 pop 到 u，这些就是一个 SCC 所有的结点
1
2
3
4
5
6
7
8
9
10
11
12
13

暴搜

沿着图上一条路径，路过的点都被选。如果出现路径上的点有冲突，则不可行