docs/graph/2-sat.md
author: chu-yuehan
SAT 是适定性（Satisfiability）问题的简称．一般形式为 k - 适定性问题，简称 k-SAT．而当 $k>2$ 时该问题为 NP 完全的．所以我们只研究 $k=2$ 的情况．
2-SAT，简单的说就是给出 $n$ 个布尔方程，每个方程和两个变量相关，如 $a \vee b$，表示变量 $a, b$ 至少满足一个．然后判断是否存在可行方案，显然可能有多种选择方案，一般题中只需要求出一种即可．另外，$\neg a$ 表示 $a$ 取反．
???+ example "洛谷 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$ 为假」．
2-SAT 问题的目标是给每个变量赋值使得所有条件得到满足．
使用布尔方程表示上述问题．设 $a$ 表示 $x_a$ 为真（$\neg a$ 就表示 $x_a$ 为假）．如果有个人提出的要求分别是 $a$ 和 $b$，即 $(a \vee b)$（变量 $a, b$ 至少满足一个）．对这些变量关系建有向图，则把 $a$ 成立或不成立用图中的点表示，$\neg a\to b$ $\neg b\to a$，表示 $a$ 不成立 则 $b$ 一定成立；同理，$b$ 不成立 则 $a$ 一定成立．建图之后，我们就可以使用缩点算法来求解 2-SAT 问题了．
| 原式 | 建图 |
|---|---|
| $\neg a \vee b$ | $a \to b$ 和 $\neg b \to \neg a$ |
| $a \vee b$ | $\neg a \to b$ 和 $\neg b \to a$ |
| $\neg a\vee\neg b$ | $a \to \neg b$ 和 $b \to \neg a$ |
许多 2-SAT 问题都需要找出如 $a$ 不成立，则 $b$ 成立 的关系．
思考如果两点在同一强连通分量里有什么含义．根据前文边的逻辑意义可知：若两点在同一强连通分量内，则这两点代表的条件 要么都满足，要么都不满足．
建图后我们使用 Tarjan 算法找 SCC，判断对于任意布尔变量 $a$，表示 $a$ 成立的点和表示 $a$ 不成立的点是否在同一个 SCC 中（同一条件不可能既满足又不满足，或既不满足又并非不满足），若有则输出无解，否则有解．
输出方案时可以通过变量在图中的拓扑序确定该变量的取值．如果变量 $x$ 的拓扑序在 $\neg x$ 之后，那么取 $x$ 值为真．应用到 Tarjan 算法的缩点，即 $x$ 所在 SCC 编号在 $\neg x$ 之前时，取 $x$ 为真．因为 Tarjan 算法求强连通分量时使用了栈，如果跑完 Tarjan 缩点之后呈现出的拓扑序更大，在 Tarjan 会更晚被遍历到，就会更早地被弹出栈而缩点，分量编号会更小，所以 Tarjan 求得的 SCC 编号相当于 反拓扑序．
算法会把整张图遍历一遍，由于这张图 $n$ 和 $m$ 同阶，计算答案时复杂度为 $O(n)$，因此总复杂度为 $O(n)$．
??? note "代码实现"
cpp --8<-- "docs/graph/code/2-sat/2-sat_3.cpp"
???+ example "HDU3062 Party" 有 $n$ 对夫妻被邀请参加一个聚会，因为场地的问题，每对夫妻中只有一人可以列席．在 $2n$ 个人中，某些人之间有着很大的矛盾（当然夫妻之间是没有矛盾的），有矛盾的两个人是不会同时出现在聚会上的．有没有可能会有 $n$ 个人同时列席？
按照上面的分析，如果 $a_1$ 中的丈夫和 $a_2$ 中的妻子不合，我们就把 $a_1$ 中的丈夫和 $a_2$ 中的丈夫连边，把 $a_2$ 中的妻子和 $a_1$ 中的妻子连边，然后缩点染色判断即可．
??? note "参考代码"
cpp --8<-- "docs/graph/code/2-sat/2-sat_1.cpp"
???+ example "2018-2019 ACM-ICPC Asia Seoul Regional K TV Show Game" 有 $k$ 盏灯，每盏灯是红色或者蓝色，但是初始的时候不知道灯的颜色．有 $n$ 个人，每个人选择三盏灯并猜灯的颜色．一个人猜对两盏灯或以上的颜色就可以获得奖品．判断是否存在一个灯的着色方案使得每个人都能领奖，若有则输出一种灯的着色方案．
根据 伍昱 -《由对称性解 2-sat 问题》，我们可以得出：如果要输出 2-SAT 问题的一个可行解，只需要在 tarjan 缩点后所得的 DAG 上自底向上地进行选择和删除．
具体实现的时候，可以通过构造 DAG 的反图后在反图上进行拓扑排序实现；也可以根据 tarjan 缩点后，所属连通块编号越小，节点越靠近叶子节点这一性质，优先对所属连通块编号小的节点进行选择．
下面给出第二种实现方法的代码．
??? note "参考代码"
cpp --8<-- "docs/graph/code/2-sat/2-sat_2.cpp"