代码 / 课件请前往：https://blog.csdn.net/wu_tongtong/article/details/78008148

问题类型

给定一类逻辑约束方程组，求解的可行性 / 解的方案。

求解可行性

缩点，判断是否矛盾。

求解方案

推导法

算法流程：

• 将图构造出来后，枚举每个点
• 若这个点没有被 marked，则枚举该点的解。先枚举这个点为 true，深搜递归标记（同时将标记的点放入栈中），如果矛盾，收回标记点，再枚举这个点为 false。若再次矛盾，则问题无解。

算法特性：
无需回溯过程。

算法复杂度：$O(nm)$

算法证明：

概念补充：
我们称 i 为 i'的反面
若 i 和 i' 是否被选都还没被决定，则我们称 i 和 i'是未盖点。否则称其为已盖点。
当一对配对结点都被加入解集，我们称该解集矛盾。

2-SAT 的建模具有对称性：原命题成立，逆否命题仍然成立。
即若有边 i ->j，则有边 j'->i'。
显然由此推导，若有路径 i ->j，则有路径 j'->i'。

假设当前一轮我们推出有 u ->p
而前一轮我们推出有 v ->p'
由对称性我们有：v->p'->u'

则我们可以得知，u 应该已经是已盖点，这与我们现在正在推导 u 的情况不符。
因此，前一轮我们并没有推出 v ->p'（即前一轮的 v 并非已盖点），而是这一轮。
即 u ->v->u'。
这就是出现矛盾的唯一情况。

当我们选择两个都矛盾的时候，问题 必定无解 。
因为有 u ->u'->u。
即我们所说的 u 与 u' 处于同一个强连通分量。

而现有的解集一定不会影响矛盾的推导，因此 没有后效性 ，这个算法 并不需要回溯 。
即，若问题有矛盾，无论你现有的解集是什么，问题总会推出是有矛盾的。
否则就总是不会推出有矛盾。
当无矛盾时，问题有解。

对称性求解

考虑一个图上的 SCC，若 SCC 中的一个点被选了显然全部的点都被选。

根据我上面的证明，推导 u 中出现矛盾是存在路径 u ->u'的充要条件。因此推导 u 点对若两次出现矛盾，则有 u ->u'->u 表示无解。

那么显然若不存在路径 u ->u'，推导 u 中就不会出现矛盾。

则若图中不存在任意 u 有 u ->u'->u，问题一定有解。

所以我们可以判断 SCC 中是否存在一对 u ->u'->u，有则判无解，否则一定有解。

考虑选择 SCC。如果我们每次选择出度为 0 的未盖点，每次由此推导需要加入解集的点只有本身，这样会使加入解集与解产生矛盾的可能消失。并且由于在之前已经判断，这样子推导是一定能够得到解的。这样是一个逆序拓扑的顺序。

我们考虑使用 Tarjan 求 SCC 的过程，发现本质上是一个 dfs 的过程。SCC 编号增加，对于一个点，若其 SCC 编号小，则一定是逆序拓扑序中靠前的，因为是弹栈的一个过程。

所以我们对于一对点可以直接比对所属 SCC 的大小，来判断是先选哪个。这样子的话这个算法就得到了一个简洁的优化。

复杂度 $O(n+m)$。