2-SAT 学习

构图

对于变量$x_i$​​​,节点$\lnot i$​​表示$x_i=False$​​,节点$2i$​​表示$i$​​.​

$x \to y$​表示如果选择了$x$​，则必须选择$y$​.注意这里的$x$​和$y$​​表示变量取0或1时代表的节点。其实就是按照逻辑连接词蕴含来理解即可。

因此我们可以处理一些逻辑关系：

$i,j$不能同时选

连接 $i \to \lnot j$​，$j \to \lnot i$​​

逻辑表达式 $a_i \;xor\;a_j=1$

$i,j$必须同时选

连接$i \to j$​,$j \to i$​​

逻辑表达式 $a_i \; xor \;a_j =0$​

$i,j$至少选一个

连接$\lnot i \to j$​​​​​​, $\lnot j \to i$​​, $i \to \lnot j$​​ , $j \to \lnot i$​​​​

逻辑表达式 $a_i | a_j=1$

$i$​​必须选

连接$\lnot i \to i$​

注意事项

1、逆否命题是需要保证的。

运行

构图结束后，在这张有向图上跑Tarjan进行缩点。那么根据上面我们对边的定义，如果如果$x_i$和$\lnot x_i$在一个SCC中，显然是无解的。

排除掉无解的情形，考虑对DAG进行拓扑排序。如果$x_i$的拓扑序比$\lnot x_i$小，那么$x_i$取False。因为不然的话会出现$1 \to 0=0$的非法情况。

此外，根据Tarjan的运行流程，并不需要真的跑拓扑排序。因为反图的拓扑序就是Tarjan生成SCC的顺序。

例题

CF 468 B

注意弄清$x$的01取值和集合划分的关系。