$SAT$理论：

$2-SAT$

两种形式：

$x in hat B$

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

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

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

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

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

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

$1.quad$原图具有对称传递性 $x ightarrow y$则$ eg y ightarrow eg x$

感觉好像逆否命题

$2.quad SCC$对称

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

如何构造一组解？

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

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

$3.$拓扑排序

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

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

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

总体复杂度$O(n)$

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

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

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

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

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