2sat

Published: April 11, 2019 by Daltao

• Categories:
• algorithm 101

• Tags:

• 2-sat算法
• 2-sat钦定变量后判断是否有解
• 2-sat判同

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：

$$f(b_1,b_2,\ldots,b_n)=(\lor{B_1})\land(\lor{B_2})\land\ldots\land(\lor{B_m})$$

问是否存在一组输入$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)$。

2-sat钦定变量后判断是否有解

我们已经知道2-sat有解等价于对应的有向图中，不存在这样的$x$，$x$与$\neg x$是否处于相同连通块中。

给定一个2-sat表达式，在表达式成立的前提下，我们需要回答$q$个询问，询问分如下几类：

1. 给定$k$个不同的布尔变量$x_1,\ldots,x_k$。判断是否可以将它们同时设为$x$为true。

其中2-sat变量总数为$n$，条件数为$t$。满足$1\leq n\leq 10^3$，$1\leq m,q\leq 10^6$，且所有请求中出现的布尔变量的总数不会超过$10^6$。

首先有解的前提必定是在无附加条件的情况下，2-sat是有解的，换言之任意布尔变量和它的逆变量都不在相同的强连通分量中。

很显然每次重新构图跑Tarjan算法是不现实的。我们可以对一开始的条件构图，并通过Floyd算法跑传递闭包，利用bitset可以优化到$O((2n)^3/32)$。

如果存在某个$x_i$到$\neg x_j$有路径，则一定无解。如果前面条件不成立，则一定有解。无解的情况是显然的，$x_i$的成立需要$x_j$不成立，但是请求要求二者同时成立，这自然是不可能达成的。在路径不存在的情况下，考虑钦定这些变量带来的影响，实际上是从向图中加入$k$条边$(\neg x_i, x_i)$。如果出现新环，则必定至少包含其中的一条边。如果只含一条边$(\neg x_j,x_j)$，这意味着原图中$x_j$到$\neg x_j$有路径，这与前提相悖。如果含至少两条边，则不妨认为最早出现的两条边为$(\neg x_1,x_1)$和$(\neg x_2,x_2)$，这意味着原图中$x_1$到$\neg x_2$有一条路径，这依旧与前提相悖。因此加入这些边一定不会出现新的环，故也不会产生新的强连通分量，整个图依旧有解。

我们可以用bitset来处理请求，时间复杂度为$O(kn/32)$。

总的时间复杂度为$O(m+\frac{n^3}{4}+\frac{n}{32}\sum_k)$，还是很快的。

上面这个问题同时还告诉了我们，对于任意非钦点的布尔变量，都存在一种使表达式成立的方案使其为true或false。

2-sat判同

考虑两个2-sat表达式$A,B$。布尔变量总数为$n$，条件数为$m$，其中$1\leq n\leq 10^3$，$1\leq m\leq 10^6$。要求$A$是否等于$B$。两个表达式相同，当且仅当对于所有$2^n$种条件变量的赋值方案$x$，都有$A(x)=B(x)$。

提供一道题目。

首先如果$A,B$是无解的，则显然成立，否则如果仅一者有解，则显然不成立。否则$A,B$同时有解，我们下面进行讨论。

首先如果两边存在不同的钦定点（值不同，或者一边钦点，一边不钦点），那么一定不等。下面我们忽略钦定点，仅考虑非钦定点。

我们用Floyd算法找依赖闭包，如果$A$和$B$所有变量的依赖关系都相同，那么显然是相同的。否则不妨设在$A$中$x$对$y$存在依赖关系，但是在$B$中不存在。这时候我们可以将$x$和$\neg y$钦定为true，这时候$A$一定不成立。但是考虑到$x$到$y$无路径，同时$\neg y$到$\neg x$无路径（我们的图是对称的，$x\rightarrow y \Leftrightarrow \neg y\rightarrow \neg x$），这时候根据2-sat钦定变量后判断是否有解这一节的内容可知，可以找到一组赋值方案使$B$成立。

这里时间复杂度为$O(\frac{n^3}{4}+m)$。