这种一看就很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)$