2-SAT Notes

ajcxsu
ajcxsu 2018年08月20日
  • 25 次阅读

代码/课件请前往: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://acxblog.site/archives/2-sat.html
本文采用 CC BY-NC-SA 3.0 协议进行许可