参考了这个Blog
$O(nm)$ 算法
假设一个点取 0，并且顺着往下标记；如果有矛盾，假设它取 1，再标记。如果取 0 或者 1 都不行，可以证明问题无解。
代码：
- 用感叹号标记的行对应于输出方案。
- 注意从 $0$ 开始标号较为方便，此时输入编号后要减 $1$ .
- 点数是从句数目的两倍！
bool dfs(int u) {
if(vis[u]) return true;
if(vis[u^1]) return false;
sel[(u >> 1)] = u & 1; // !
vis[u] = true; stk[++stk[0]] = u;
for(size_t j = 0; j < G[u].size(); j++)
if(!dfs(G[u][j])) return false;
return true;
}
bool solve() {
static int p[MAXN+10]; // mapping
for(int i = 0; i < n; i++) p[i] = i;
random_shuffle(p, p + n);
for(int i = 0; i < 2 * n; i++) {
random_shuffle(G[i].begin(), G[i].end());
}
for(int cur = 0; cur < n; cur++) {
int i = p[cur];
if(!vis[i<<1] && !vis[i<<1|1]) {
stk[0] = 0; sel[i] = 0; // !
if(!dfs(i<<1)) {
for(; stk[0]; --stk[0])
vis[stk[stk[0]]] = false;
sel[i] = 1; // !
if(!dfs(i<<1|1))
return false;
}
}
}
return true;
}
$O(m)$ 算法
暂时没能理解……过几天看看
建模
一定要连接反向边！！！！！
| Clause | Edge(s) |
|---|---|
| $x = y$ | $x \rightarrow y, y \rightarrow x, \neg x \rightarrow \neg y, \neg y \rightarrow \neg x$ |
| $x \neq y$ | $\lnot x \rightarrow y, \lnot y \rightarrow x, x \rightarrow \lnot y, y \rightarrow \lnot x$ |
| $x = 0 \; / \; x = 1$ | $x \rightarrow \neg x \; / \; \neg x \rightarrow x$（别忘了反向边！） |
| $(x = a) \lor (y = b)$ | $(x = \neg a) \rightarrow (y = b), (y = \neg b) \rightarrow (x = a)$ |
| $(x = a) \land (y = b)$ | 拆成两个 $``x = 0 \; / \; x = 1”$ 形式 |
例题
Now or later
二分答案，转为判定性问题，用 xor 建立 2-SAT 即可。
Astronauts
以选不选 C 作为变量建立 2-SAT 模型，然后就是裸题了。
[NOI2017] 游戏
首先爆搜出 x 位置不能填写什么。由于 3-SAT 问题是 NP-Hard 的，我们需要转化为 2-SAT.
我们考虑每个位置。除开不能用的车类型后，对于另外两类我们可以重标号。再考虑题中每个规则 $(i, h_i, j, h_j)$ 的限制。考虑对于每个 $i$ ，如果 $h_j$ 对于 $j$ 是可选的，就连边（一定不能忘记反向边）；否则表示 $i$ 不能选取 $h_i$ .
发现 $n \le 5 \times 10^5$ ，所以直接跑 $O(nm)$ 的 2-SAT 是不能承受的。一种方法是使用线性 2-SAT 算法。还有一个方法：按照随机顺序选择 2-SAT 的起点。这样实测也跑的飞快。
