2-SAT 问题学习笔记

问题

给定 $n$ 个变量与 $m$ 个等式，每个变量只能为 $false$ 或是 $true$ ，每个等式都至多有两个变量 $x_i , x_j$ ，并且等式右边给出这两个变量通过至多一个位运算符运算得到的结果，形如：

$$x_1\ and\ x_ 2 = false \\ x_2\ or\ x_3 = true \\ x_3\ xor\ x_1 = false \\ x_2 = true$$

判断是否有解

可以将这个问题转化为求强连通分量问题，首先这张图的点为每个 $x_i$ 的两种状态，如果根据第 $k$ 个等式， 知道 $x_i$ 一定能够推出 $x_j$ 的值，例如 $x_1 and x_2 = false$ ，当 $x_1 = true$ 时一定能得到 $x_2 = false$ ，则从 $x_i$ 的 $false$ 点连向 $x_j$ 的 $true$ 点，又例如 $x_2 = true$ ，则从 $x_2$ 的 $false$ 点连向 $x_2$ 的 $true$ 点，表示一定能从 $x_2 = false$ 推到 $x_2 = true$。

然后对建起来的这张有向图求一个强连通分量，如果存在任意强连通分量包含 $x_i$ 的两个点，则无解，否则有解。