说在前面
本文大多数参照作者的理解思考，可能存在偏差，欢迎讨论/纠正。
Pt.1 问题引入：满汉全席
现在你正在参加一个厨艺大赛。你面前有 $ n $ 种材料，每种必须选择采用满式做法还是汉式做法。
评委席上坐着 $ m $ 位呆萌可爱的奶龙。每个奶龙会有两个偏好，具体表现为某种材料必须采用满式/汉式（如材料3必须采用汉式，材料7必须采用满式等），只要满足其中的任意一个偏好你就可以获得奶龙的赞赏并得到一个通过。
只有全部通过才能当上厨神（？），所以我们需要求出是否有一个方案使得所有评审都通过。
实际上，这就是一个经典的 2-SAT 模型：
每个变量有两种取值，每个约束都关联两个变量，且要求「至少一个成立」。
Pt.2 如何解决
有一个很显而易见的暴力做法： 01DFS ，将每个材料做满式/汉式的情况都枚举一遍。
总方案数为 $ 2 ^ n $ ，当 $ n $ 稍微大一点的时候这个做法的效率劣势就会变得非常明显。
所以我们不能暴力，而是应当采用一个更高效的方法。
我们可以对比一下。其实，暴力的本质就是在所有方案中搜索，而 2-SAT 则是将问题转化为一个图，用图来描述一种强制关系（也就是一个选择会强制哪些其它选择）并用图论的工具来检查是否矛盾以及构造方案。
Pt.3 如何 2-SAT
上面也说了，其实 2-SAT 本质就是将选择之间的关系转化为图。
具体地，我们发现如果我们要满足所有评审，假如说一个选择是 $ A $，另一个选择是 $ B $，那么如果我们不选 $ A $ 的话为了满足所有评审就一定要选 $ B $ 。
所以我们可以对所有的这种强制关系建边，具体地，对于所有 $ A $ 与 $ B $ ，我们建两条边即 \(\neg A \to B\) 与 \(\neg B \to A\) ；
建模完了，然后捏？
烧烤一下，什么情况会导致我们无法满足所有评审？而且这样建图不会让 $\neg A $ 与 $ A $ 互相可达么？那这个图不就飞了吗？
发现了吗？其实这种 $\neg A $ 与 $ A $ 互相可达的情况就是无解。因为这意味着你要是不选 $ A $ 你就必须选 $ A $ ，如果你选了 $ A $ 你就必须不选 $ A $ ，这不就无解了么。
但是如何判断呢？
前面我们介绍了，2-SAT是用图来描述一种强制关系并用图论的工具来检查是否矛盾以及构造方案。现在我们先思考是否矛盾。
回忆一下什么东西是有互相可达/连通的关键词的。于是我们考虑 Tarjan 求个强连通分量。
具体的，我们求出所有点所在的强连通分量，然后针对每个选择判断选/不选是否在同一个强连通分量里，如果是的话说明两者连通，即无解。
但是实现又是一个问题。我在和小蓝鱼对话的时候了解到了一个 trick :异或。
具体的，对于每一个 $ i $ 有：
- $ 2i \oplus 1 = 2i + 1 $
- $ 2i + 1 \oplus 1 = 2i $
这样就可以轻松实现对于选/不选的转化。
所以我们可以写一个 get_node 函数，用来获取每个选择所对应的图的点的编号，同时实现上面那个东东。
好了，现在判断的实现问题也解决了，但是如何构造具体方案呢？
我们可以用 Tarjan 缩点，并进行拓扑排序。在拥有合法方案的情况下，每个 $\neg A $ 与 $ A $ 一定是不在同一个强连通分量里的。那么如果我们选拓扑序小的点，它可能会走到拓扑序大的点从而引发矛盾。所以我们对于每个 $\neg A $ 与 $ A $ 取拓扑序更大的点就可以构造出一个合法方案了。
Pt.4 实战
有点没时间写先咕一咕，等有时间了再回来补上。