这种一看就很2的东西....

---

 

参考资料:

  

 

---

 

$SAT$理论：  

$2-SAT$

两种形式：

$x \in \hat B$

$x \lor y(x,\ y \in B)$

对于第二种形式，$x \lor y\ =\ \neg(\neg x \land \neg y)$

增加有向边$(\neg x,y)\quad (\neg y,x)$

显然一个强连通分量中的点会被同时选择或不选

因此$b_i$和$\neg b_i$不能在同一个$SCC$中，我们通过求$SCC$就可以判断可行性了

 

由上可知这个图是对称的，表现：

$1.\quad$原图具有对称传递性 $x \rightarrow y$则$\neg y \rightarrow \neg x$

感觉好像逆否命题

$2.\quad SCC$对称

$3.\quad x$的后代对称于$\neg x$的前代

 

如何构造一组解？

$1.$求$SCC$，缩点边反向

$2.$记录每个原图的点$x$的$\neg x$，可以发现一个$SCC$只会有一个否定，因为图是对称的，$SCC$中所有点的否定的$SCC$是相同的

$3.$拓扑排序

$4.$选第一个未染色的点(这里指$SCC$)，染白色，然后将否定点及其后代染黑色

$5.$重复上述过程直到染色完成

最后所有白色的点就是一组解

总体复杂度$O(n)$ 

 

$Naive$做法

求$SCC$的做法复杂度很优秀，但只能判断可行性和构造一组解

对于一些题目不能很好的处理

而$naive$做法就是选择一个没有赋值的变量，赋值为真，然后$dfs$下去，看看是否会冲突(一个点和否定点都为真)

这样就非常灵活了，因为选择一个变量的值的权力掌握在我们手上

复杂度最坏可能变为$O(nm)$