什么是2-sat问题

有n个布尔型变量xi,另外m个需要满足的条件。每个条件都是“xi为真/假或者xj为真/假”。这句话中的“或者”意味着两个条件中至少有一个正确。2-sat问题的目标是给每个变量赋值,使得所有的条件得到满足。

算法的大致过程是这样的:

构造一张有向图G,其中每个变量拆成两个结点2i和2i+1,分别表示xi为假和xi为真。最后要为每个变量选其中一个结点标记。

对于每个“xi为假或者xj为假"这样的条件,我们连两条对称的有向边。我们上面说过,或者意味着两个中间至少有一个正确。所以如果xi为真的话,那么xj一定为假,所以我们从2*i+1向2*j连一条有向边。同样的道理,我们也从2*j+1向2*i连一条有向边。

接下来我们逐一考虑每个没有赋值的变量,设为xi。我们先假定它为假,然后标记结点2i,并且沿着有向边标记所有能标记的结点。如果标记的过程中发现某个变量对应的两个结点都被标记,则xi假这个假定不成立,需要改为xi为真,然后重新标记。

模板代码如下

code from LRJ

 /*
将每个变量拆成两个点2i和2i+1,分别表示xi为假和xi和真
对于每个条件,连两条对称的有向边。
逐一考虑没有赋值的变量,先假定它为假,然后标记结点2i,然后沿着有向边标记所有能标记的结点
如果标记的过程中 发现某个变量对应的两个结点都被标记,则xi为假这个假定不成立,需要改xi为真
然后重新标记
*/
#include <cstdio>
#include <cstring>
#include <algorithm>
#include <iostream>
#include <vector> using namespace std;
const int maxn=+;
struct TwoSAT{
int n;
vector<int>G[*maxn];
bool mark[maxn*];
int S[maxn*],c;
bool dfs(int x){
if(mark[x^])return false;
if(mark[x])return true;
mark[x]=true;
S[c++]=x;
for(int i=;i<G[x].size();i++){
if(!dfs(G[x][i]))return false;
}
return true;
}
void init(int n){
this->n=n;
for(int i=;i<n*;i++)G[i].clear();
memset(mark,,sizeof(mark));
}
void add_clause(int x,int xval,int y,int yval){
x=x*+xval;
y=y*+yval;
G[x^].push_back(y);
G[y^].push_back(x);
} bool solve(){
for(int i=;i<n*;i+=){
if(!mark[i]&&!mark[i+]){
c=;
if(!dfs(i)){
while(c>)mark[S[--c]]=false;
if(!dfs(i+))return false;
}
}
}
return true;
}
};
int main(){
return ;
}
05-11 21:51
查看更多