2-SAT
这个模型给出了 $n$ 个布尔变量, $m$ 个限制条件,每个限制条件规定两个变量的关系( $u=x\vee v=y$ )。要求找出一组解。
构图
给每个变量建两个点,一个表示变量为真( $u=1$ ,这里用 $u$ 表示)一个表示变量为假( $u=0$ ,用 $u'$ 表示)。对于一个条件 $u=x\vee v=y$ ,若 $u\ne x$ 则 $v=y$ ,反之亦然,以 $u=1\vee v=0$ 为例,对于两个变量分别建条边 $u'\rightarrow v',v\rightarrow u$ 表示,如果 $u=0$ 则 $v=0$ 、如果 $v=1$ 则 $u=1$ ,边表示如果这个那么一定那个。很明显有对称性,所以反着建图也可以,不过要注意意义。
显然,同一强连通分量内的变量值一定是相等的。于是强连通分量缩点即可。
求解时,拓扑序先后就可以确定这个值真假。