2sat

Published: by Creative Commons Licence

  • Tags:

2-sat原理

假设有若干个布尔变量,我们记为$b_1,b_2,\ldots,b_n,\neg{b_1},\neg{b_2},\ldots,\neg{b_n}$。很显然总共有$2^n$种赋值方案。

若我们增加一些限制条件,假设有若干个集合${b_1,b_2,\ldots,b_n}$集合的子集集合的子集$B_1,B_2,\ldots,B_m$,记$\lor{B_i}$表示$B_i$中的所有变量的并,定义函数中的所有变量的并,定义函数中的所有变量的并,定义函数中的所有变量的并,定义函数f:

问是否存在一组输入$b_1,b_2,\ldots,b_n$,能使得$f(b_1,b_2,\ldots,b_n)=true$。如果有,就找到任意一组可行的解。

如果$max({|B_1|,|B_2|,\ldots,|B_m|})\leq k$,那么就称这是$k-satisfication$问题。很显然$k$越大,解决的难度也越大。由于当$k>2$时$k-sat$问题是NP的,因此我们仅考虑解决$2-sat$问题。

我们可以对应建立$2n$个顶点将其转换为图论问题。逻辑学中,$a\lor b$等价于$\neg{a}\rightarrow b \land \neg{b}\rightarrow a$,对应的,我们在我们图中加入两条单向边$(\neg{a},b)$和$(\neg{b},a)$。在这里单向边表示一种依赖关系,若一个顶点$u$到另外一个顶点$v$之间存在一条路径,那么就认为$u$只有在$v$成立(为$true$)的前提下才能成立。

图建立完成后,这时候我们的图应该是一幅有向带环图。考虑到环意味着循环依赖,即环中的顶点要么同时成立,要么同时不成立。我们可以利用Tarjan算法搜索图中的所有强连通分量,之后将强连通分量缩为一个点。

下面介绍如何判别$2-sat$问题有解。非常简单,如果存在变量$b_i$和$\neg{b_i}$处于同一个强连通分量,那么该问题无解,否则有解。很显然如果这样一对互逆变量存在同一个强连通分量中,那么两者的值应该是相同的,但是这样一对变量的值永远一个为真一个为假,因此就产生了悖论,故无解。那么如果保证任何强连通分量中不含互逆变量就一定有解呢,我们下面将提出在这种情况下一定能成功构造一组解的方法。

首先我们进行缩点后,图中就不存在环了。我们可以对图进行拓扑排序,没有出边的点放在最前。之后我们按先后顺序处理顶点,如果顶点的逆顶点被处理过了,我们就将顶点的值设置为$false$,否则设置为$true$。

下面我们说明这个算法的正确性,需要满足下面条件:

  1. 所有顶点与其逆顶点拥有不同值
  2. 设置为true的顶点所依赖的所有顶点的值也都是true

对于任意顶点$u$与$\neg{u}$,由于二者必然有先后的处理顺序,先处理的会被赋值为$true$,后被处理的会被赋值为$false$,因此不会产生冲突。第一个条件满足。而考虑如果图中存在边$(\neg{u},v)$,就意味着存在推导关系$\neg{u}\rightarrow v$,对应的存在一个等价的逆否命题$\neg{v}\rightarrow u$,这意味着边$(\neg{v},u)$存在于图中。当我们将某个顶点$u$设置为真时,假设存在一个$u$依赖的顶点$v$且$v$被设置为$false$,而我们可以将$u$设置为真意味着$\neg{u}$还没有被处理过,而由于$(\neg{v},u)$的存在,因此$\neg{v}$也还没有被处理过,即我们在处理$v$的时候,由于$\neg{v}$未被处理过,因此$v$一定会被设置为$true$,而这与前提相悖,因此假设不成立,条件2得证。

判断是否有解以及获得一组可行解,我们只需要执行一次Tarjan算法进行缩点,再执行一次拓扑排序,最后扫描所有的顶点即可,总的时间复杂度为O(n+m)。