2-SAT Notes
代码 / 课件请前往: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)$。
本文链接:https://pst.iorinn.moe/archives/2-sat.html
许可: https://pst.iorinn.moe/license.html若无特别说明,博客内的文章默认将采用 CC BY 4.0 许可协议 进行许可☆