2-SAT

2-SAT一般给出$n$个布尔变量（取0或者取1），再给出$m$个关于这些布尔变量的约束条件（见下文），求出是否能找到解满足这些约束条件。

2-SAT可以建图，转换成强连通分量进而判断矛盾问题。对于布尔变量，只有2个取值，取0或者取1，所以对于任意一个布尔变量$x_i$，我们可用其原变量$i$（即取1值）和其反变量$i'$（即取0值）依据约束条件来构建图。

约束条件

我们以变量$x_i、x_j$为例，$i、j$表示原变量，$i’、j'$表示反变量。一般来说，2-SAT约束条件有以下几种。

1. 必须$x_i$.
2. 必不选$x_i$。
3. $x_i$与$x_j$中选择一个。
4. $x_i$与$x_j$不都选。
5. $x_i$与$x_j$选择情况相同。
6. $x_i$与$x_j$选择情况相反。

下面依次看这几种约束条件的构图。

1. 必选$x_i$。等价于$x_i = 1$。此种选择方法有多种构图的形式，其中一种就是我们不连边，最后看$x_i$是否等于1，或者说当$x_i$等于1时是否存在解。还有一种方法是我们连一条$i'-i$的边。其意思为当我们推断出$x_i$为0的时候，那么$x_i$一定为1。由于我们判断是否有解是根据强连通分量来的，所以这样的连边并不矛盾。
2. 必选$x_i$。等价于$x_i = 0$。连$i-i'$的边即可。
3. $x_i$与$x_j$中选择一个。等价于$x_i \lor x_j = 1$。连边$i'-j、j'-i$。
4. $x_i$与$x_j$不都选。等价于$x_i \land x_j = 0$。连边$i - j'、j-i'$。
5. $x_i$与$x_j$选择情况相同。等价于$x_i \ XOR \ x_j = 0$。连边$i-j、j-i、i'-j'、j'-i'$。
6. $x_i$与$x_j$选择情况相反。等价于$x_i \ XOR \ x_j = 1$。连边$i-j'、j-i'、i'-j、j'-i$。

判定与解的输出

构图完成之后，即可进行有解性判定。

使用tarjan算法求出强连通分量并染色，如果有一个布尔变量的原变量和反变量在一个scc中，那么原问题无解，否则一定存在解。

若求任意解，则对染色后的图重新建图，但是把边反向，统计入度，做拓扑排序，同时求出每个点反变量的颜色。之后按照拓扑排序的顺序，依次将对应scc标记为1以表示选中，其反变量对应的scc标记为2以表示不选中（也表示其反变量选中）。最后遍历一遍布尔变量的原变量和反变量：若变量所在的scc被标记为1，则表明选中变量；否则表示其另外一个变量被选中。

若求字典序最小的解，也使用标记法。对所有变量进行遍历，若 $x_i$ 其原变量和反变量都没进行标记过，则dfs进去优先标记 $x_i$ 的原变量，并根据他们连过的边，继续dfs标记。如果标记的过程中，某个变量的原变量和反变量同时被标记，则表示选中$x_i$的原变量无解，进而选中$x_i$的反变量继续标记。若在遍历过程中，发现无论标记某个遍历的原变量和反变量都无解，表示整个2-SAT无解。否则标记的就是字典序最小的解。