一.什么是 \(\text{2-SAT}\)
\(SAT\) 是适定性 \(Satisfiability\) 问题的简称。一般形式为 \(k -\)适定性问题，简称 \(\text{k-SAT}\)。而当 \(k>2\) 时，该问题为 \(NP\) 完全的。所以我们只研究 \(k=2\) 的情况。
形象地来说，给定 \(n\) 个布尔变量 \(a_i\)，同时给出若干个约束条件：
\((\text{not})a_i\) \(op\) \((\text{not})a_j = \text{true/false}\)。
而求解 \(\text{2-SAT}\) 就是求出一组 \(a_i\) 的解。
二.将 \(\text{2-SAT}\) 问题转换为图论问题
首先定义一条有向边的定义 \(x\to y\)：如果满足 \(x\) 就必须满足 \(y\)。
发现一个点有两个状态真或假，可以想到将点 \(u\) 拆为点 \(u_0,u_1\)，分别表示假或真。
\(1.\) \(a\land b = \text{true}\) \(\to (a1, b1),(b1, a1)\)。
\(2.\) \(a\land b = \text{false}\) \(\to (a1, b0),(b1, a0)\)。
\(3.\) \(a\lor b = \text{true}\) \(\to (a0, b1),(b0, a1)\)。
\(4.\) \(a\lor b = \text{false}\) \(\to (a0, b0),(b0, a0)\)。
这样我们就将 \(\text{2-SAT}\) 问题转换为图论问题了，可以运用图论的方式解决。
三.解决 \(\text{2-SAT}\) 问题
-
\(1.\) 判断有无解
由上文定义的状态可以得知，\(u_0\) 和 \(u_1\) 不能同时被满足。
那么存在点 \(x_0\) 和 \(x_1\) 在同一个强连通分量中时，那么无解。
反之则有解。 -
\(2.\) 求方案
由我们的建边可得：对于每个点 \(u\)，选择其拓扑序较大的那种状态更优。
为什么呢？
如下图所示：对于 \(x1\) 的两种状态，如果选择 \(\text{false}\)，那么推导出 \(x2\) 为 \(\text{true}\)，又推导出 \(x1\) 为 \(\text{true}\)，又推导出 \(x2\) 为 \(\text{false}\)，发现这种解法矛盾了。
但如果对于 \(x1\) 选择 \(\text{true}\)，那么 \(x2\) 为 \(\text{false}\)，则满足要求。
由此我们得出：对于每个点 \(u\)，选择其拓扑序较大的那种状态更优。
这里不需要再做一遍拓扑排序求拓扑序，在 \(\text{Tarjan}\) 求强连通分量中就求出了每个点的逆拓扑序，每个点的强连通分量编号也就是逆拓扑序。