2-SAT

· · 个人记录

\texttt{2-SAT}

\texttt{P, NP, NPC}

$\texttt{NP:}$ 不能在多项式时间内解决或不确定能不能在多项式时间内解决，但是能在多项式时间验证的问题。 $\texttt{NPC:}$ NP完全问题，所有NP问题在多项式时间内都能约化到它的NP问题，即解决了此NPC问题，所有的NP问题也都得到解决。 $\texttt{NP hard:}$ NP难问题，所有NP问题在多项式内都能约化到它的问题（不一定是NP问题） ![PNPNPC](https://cdn.luogu.com.cn/upload/image_hosting/2i22evyb.png) ### $\texttt{2-SAT}$ 问题 #### $\texttt{SAT}$ 问题 例如： 有 $n$ 个 $\texttt{bool}$ 变量 ${x1, x2, … , x????}$ ,取值为 $0/1$； 有 $m$ 个逻辑表达式，形如 ```{x1&x2|x3=1,x1^x2=0}```。 问是否存在一组合法取值使得m个表达式都成立 暴力时间复杂度为 $O(nm2^n)$（枚举每个$x$的值$(2^n)$，验证逻辑表达式是否满足 $(nm)$） #### $\texttt{2-SAT}$问题 有$n$个变量${x1, x2, … , xn}$，取值为$0/1(或i和~i必取到其中一个)$; 有$m$个约束条件，每个约束条件形如: 若$x_i$取$i$(或$~i$)，则$x_j$必取$j$ (或$~ j$)。 问是否存在一组合法取值使得$m$个表达式都成立。 问题的另一种描述：给出$n$个集合，每个集合有两个元素，已知若干个条件 $<a,b>$，表示 $a$与 $b$ 矛盾（$a$与$b$属于不同集合）。从每个集合选择一个元素，判断能否一共选$n$个两两不矛盾 判定方法 1、建立2N个点的有向图，$i$和$~i$一般设为$i$和$i+N

2、对于每个约束条件连2条有向边，原问题和逆否命题，比如i->j和~i->~j
例：n个点先拆成2n个点，1,~1,2,~2,…,n,~n。i&j=0这个条件可以转化成i->~j和j->~i。
3、Tarjan算法求出有向图的scc。
4、若存在某个变量x_i，i和~i属于同一个SCC则问题无解，否则问题有解。
算法复杂度O(N+M)

2-SAT$问题有解的充分必要条件是∀$i$，$i$和$~i$不在同一个$SCC

命题转换：
a&b = 0 a\to~b,b\to~a
a&b = 1 ~a\to a,~b\to b a|b = 0 a\to~a,b\to ~b
a|b = 1 ~a\to b,~b\to a
a^b = 0 a\to b,~a\to ~b, b\to a, ~b\to ~a
a^b = 1 a\to ~b,~a\to b, b\to ~a,~b\to a

此处借用 @Anguei的介绍：

什么是 2-SAT？

首先，把「2」和「SAT」拆开。SAT 是 Satisfiability 的缩写，意为可满足性。即一串布尔变量，每个变量只能为真或假。要求对这些变量进行赋值，满足布尔方程。
举个例子：教练正在讲授一个算法，代码要给教室中的多位同学阅读，代码的码风要满足所有学生。假设教室当中有三位学生：Anguei、Anfangen、Zachary_260325。现在他们每人有如下要求：

我们不妨把三种要求设为 a,b,c，变量前加 \neg 表示「不」，即「假」。上述条件翻译成布尔方程即：(\neg a\vee b\vee\neg c) \wedge (a\vee b\vee\neg c) \wedge (\neg a\vee\neg b\vee c)。其中，\vee 表示或，\wedge 表示与。（就像集合中并集交集一样）

现在要做的是，为 ABC 三个变量赋值，满足三位学生的要求。
Q: 这可怎么赋值啊？暴力？
A: 对，这是 SAT 问题，已被证明为 NP 完全 的，只能暴力。
Q: 那么 2-SAT 是什么呢？
A: 2-SAT，即每位同学 只有两个条件（比如三位同学都对大括号是否换行不做要求，这就少了一个条件）不过，仍要使所有同学得到满足。于是，以上布尔方程当中的 c,\neg c 没了，变成了这个样子：(\neg a\vee b) \wedge (a\vee b) \wedge (\neg a\vee\neg b)

怎么求解 2-SAT 问题？

使用强连通分量。 对于每个变量 x，我们建立两个点：x, \neg x 分别表示变量 x 取 true 和取 false。所以，图的节点个数是两倍的变量个数。在存储方式上，可以给第 i 个变量标号为 i，其对应的反值标号为 i + n。对于每个同学的要求 (a \vee b)，转换为 \neg a\rightarrow b\wedge\neg b\rightarrow a。对于这个式子，可以理解为：「若 a 假则 b 必真，若 b 假则 a 必真」然后按照箭头的方向建有向边就好了。综上，我们这样对上面的方程建图：

原式 建图
\neg a\vee b a\rightarrow b\wedge\neg b\rightarrow\neg a
a \vee b \neg a\rightarrow b\wedge\neg b\rightarrow a
\neg a\vee\neg b\space \space a\rightarrow\neg b\wedge b\rightarrow\neg a

于是我们得到了这么一张图：

可以看到，\neg a 与 b 在同一强连通分量内，a 与 \neg b 在同一强连通分量内。同一强连通分量内的变量值一定是相等的。也就是说，如果 x 与 \neg x 在同一强连通分量内部，一定无解。反之，就一定有解了。
但是，对于一组布尔方程，可能会有多组解同时成立。要怎样判断给每个布尔变量赋的值是否恰好构成一组解呢？
这个很简单，只需要 当 x 所在的强连通分量的拓扑序在 \neg x 所在的强连通分量的拓扑序之后取 x 为真 就可以了。在使用 Tarjan 算法缩点找强连通分量的过程中，已经为每组强连通分量标记好顺序了——不过是反着的拓扑序。所以一定要写成 color[x] < color[-x] 。

时间复杂度：O(N + M)