2-SAT学习笔记

• Marvolo • 0条评论 •

定义

每个方程含有n个未知数的布尔方程组称为n-SAT问题，当n大于2的时候该问题为NP-Hard问题。当n等于2时，可以转化为图论问题求解。

解法

每一个变量拆分为两个点，代表0和1两种状态，将方程组转化为有向边，代表点之间的依赖关系，最后的方案便是选出一个点集，该点集的所有出边所连的点全在该点集内，也就是强联通分量。这些点便代表了变量的取值情况；当一个变量拆分出的两个点位于同一个强联通分量中时，说明该变量的取值相互矛盾，此时无解。

具体求解时，先根据限制条件连边，然后用Tarjan求强联通分量，再判断是否有一个变量的两个分点在一个强联通分量中即可。

举个例子，有两个变量X和Y，拆分出的点为X,X',Y,Y',其中X,Y表示变量值取1，另外两个变量代表变量值取0.假如有如下限制关系：

X|Y=1

则连边：

X'->Y,Y'->X

在这种连边情况下，如果选择点X'，则一定会选择Y，但是选择Y不一定选择X'。观察后发现，这种连边符合上面的布尔约束条件。

相关的连边情况整理如下：

X|Y=1:X'->Y,Y'->X

X\&Y=0:X->Y',Y->X'

X\&Y=1:X->Y,Y->X

X|Y=0:X'->Y',Y'->X'

X=1,Y=0:X'->Y',Y->X

X=0,Y=1:Y'->X',X->Y

X=Y:X'->Y',Y'->X',X->Y,Y->X

例题

[BZOJ1823][JSOI2010]满汉全席

题目大意：

有n个布尔变量，和m对限制条件。每对限制条件限制了两个变量的取值，当且仅当存在一种取值方案，使得每对限制条件至少满足其中一条时有解。求在这些约束条件下是否存在解。

解法：

2-SAT裸题，参考上面连边方式3-5条即可

注意清空变量。。

代码：

#include<cstring>
#include<cstdio>
#include<iostream>
#include<algorithm>
#include<vector>
#include<cmath>
#include<queue>
#include<map>
#define N 220
#define l(x) (x<<1)
#define r(x) ((x<<1)+1)
#define LL long long
#define INF 0x3f3f3f3f
using namespace std;

int n,m,i,d,dp,cnt,T;
int tag[N],dfn[N],low[N],f[N],z[N];
char a[20],b[20];
vector <int> son[N];

inline int Abs(int x){return (x<0)?-x:x;}
inline void Swap(int &x,int &y){x^=y^=x^=y;}
inline int Min(int a,int b){return (a<b)?a:b;}
inline int Max(int a,int b){return (a>b)?a:b;}

inline int read(){
    int p=0;    char    c=getchar();
    while (c<48||c>57)  c=getchar();
    while (c>=48&&c<=57)    p=(p<<1)+(p<<3)+c-48,c=getchar();
    return p;
}

inline void Find(int x){
    ++cnt;
    while (z[dp]!=x){
        tag[z[dp]]=cnt; f[z[dp]]=0; z[dp--]=0;
    }
    tag[x]=cnt; f[z[dp]]=0; z[dp--]=0;
}

inline void Tarjan(int x){
    int i=0;
    dfn[x]=low[x]=++d;  f[x]=1; z[++dp]=x;
    for (i=0;i<son[x].size();i++)
        if (!dfn[son[x][i]]){
            Tarjan(son[x][i]);
            low[x]=Min(low[x],low[son[x][i]]);
        }   else if (f[son[x][i]])
            low[x]=Min(low[x],dfn[son[x][i]]);
    if (low[x]==dfn[x]) Find(x);
}

inline void Ready(){
    int i=0,j=0,p=0,q=0,x=0,y=0;
    memset(tag,0,sizeof(tag));  memset(z,0,sizeof(z));
    memset(dfn,0,sizeof(dfn));  memset(low,0,sizeof(low));
    memset(f,0,sizeof(f));  d=dp=cnt=0;
    for (i=1;i<=2*n;i++)    son[i].clear();
    for (i=1;i<=m;i++){
        scanf("%s%s",&a,&b);
        p=(a[0]=='m')?0:1;  q=(b[0]=='m')?0:1;
        x=y=0;
        for (j=1;j<strlen(a);j++)   x=(x<<3)+(x<<1)+a[j]-48;
        for (j=1;j<strlen(b);j++)   y=(y<<3)+(y<<1)+b[j]-48;
        if (p+q==2){
            son[x+n].push_back(y);  son[y+n].push_back(x);
        }   else
        if (p+q==0){
            son[x].push_back(y+n);  son[y].push_back(x+n);
        }   else 
        if (p==1){
            son[x+n].push_back(y+n);    son[y].push_back(x);
        }   else {
            son[y+n].push_back(x+n);    son[x].push_back(y);
        }
    }
}

inline void Work(){
    int i=0;
    for (i=1;i<=2*n;i++)
    if (!dfn[i])    Tarjan(i);
    for (i=1;i<=n;i++)
    if (tag[i]==tag[i+n]) {
        printf("BAD\n");    return;
    }
    printf("GOOD\n");
}

int main(){
    scanf("%d",&T);
    while (T--){
        scanf("%d%d",&n,&m);
        Ready();    Work();
    }
    return 0;
}

[Kattis]Ghostbusters 2

题目大意：

在平面上有n个整点，每个整点需要选择一种攻击方向(横或者纵)，所有整点有一个共同的整数攻击半径R，每个点的攻击范围是该点沿攻击方向向两边延伸R个单位。为使所有点的攻击范围互不重合，求R的最大值。

解法：

春训团队赛的一道题。

首先设横向攻击为1，纵向攻击为0。然后二分R，如果有同一列两个点不可同时纵向攻击，则构造方程

X|Y=1

如果有同一行两个点不可同时横向攻击，则构造方程

X\&Y=0

之后按照2-SAT解法求是否有合法方案即可。

代码：

#include<cstring>
#include<cstdio>
#include<iostream>
#include<algorithm>
#include<vector>
#include<cmath>
#include<queue>
#include<map>
#define N 8010
#define l(x) (x<<1)
#define r(x) ((x<<1)+1)
#define LL long long
#define INF 0x3f3f3f3f
using namespace std;

int i,n,cnt,dp,d;
int x[N],y[N],low[N],dfn[N],z[N],f[N],v[N],tag[N],l[N];
vector <int> son[N];

inline int Abs(int x){return (x<0)?-x:x;}
inline void Swap(int &x,int &y){x^=y^=x^=y;}
inline int Min(int a,int b){return (a<b)?a:b;}
inline int Max(int a,int b){return (a>b)?a:b;}

inline int read(){
    int p=0;    char    c=getchar();
    while (c<48||c>57)  c=getchar();
    while (c>=48&&c<=57)    p=(p<<1)+(p<<3)+c-48,c=getchar();
    return p;
}

inline void Ready(){
    int i=0,j=0;
    for (i=1;i<=n;i++)
        for (j=1;j<=n;j++)
            if (x[i]==x[j]&&i!=j){
                l[i]++; break;
            }
    for (i=1;i<=n;i++)
        for (j=1;j<=n;j++)
            if (y[i]==y[j]&&i!=j){
                l[i]++; break;
            }
    for (i=1;i<=n;i++)  l[i]=(l[i]==2)?1:0;
}

inline void Work(int x){
    cnt++;
    while (z[dp]!=x){
        tag[z[dp]]=cnt; f[z[dp--]]=0;
    }
    tag[x]=cnt; f[z[dp--]]=0;
}

inline void Tarjan(int x){
    int i=0;
    dfn[x]=low[x]=++d;  z[++dp]=x;  f[x]=1;
    if (son[x].size())
        for (i=0;i<son[x].size();i++)
            if (!v[son[x][i]]){
                v[son[x][i]]=1; Tarjan(son[x][i]);
                low[x]=Min(low[x],low[son[x][i]]);
            }   else
            if (f[son[x][i]])   low[x]=Min(low[x],dfn[son[x][i]]);
    if (low[x]==dfn[x]) Work(x);
}

inline bool Check(int t){
    int i=0,j=0;
    for (i=1;i<=2*n;i++)    son[i].clear();
    memset(low,0,sizeof(low));  memset(dfn,0,sizeof(dfn));
    memset(f,0,sizeof(f));  memset(v,0,sizeof(v));
    memset(tag,0,sizeof(tag));  memset(z,0,sizeof(z));
    dp=cnt=d=0;
    for (i=1;i<=n;i++)
        for (j=i+1;j<=n;j++){
            if (l[i]+l[j]!=2)   continue;
            if (x[i]==x[j]&&2*t>=Abs(y[i]-y[j])){
                son[n+i].push_back(j);  son[n+j].push_back(i);
            }
            if (y[i]==y[j]&&2*t>=Abs(x[i]-x[j])){
                son[i].push_back(n+j);  son[j].push_back(n+i);
            }
        }
    for (i=1;i<=2*n;i++)
        if (!v[i]&&l[i]){
            v[i]=1; Tarjan(i);
        }
    for (i=1;i<=n;i++)
        if (l[i]&&tag[i]==tag[i+n]) return 0;
    return 1;
}

inline void Work(){
    int i=0,j=0,low=0,high=INF,mid=0;
    if (Check(INF)) {
        cout<<"UNLIMITED"<<endl;
        return;
    }
    while (low<=high){
        mid=(low+high)>>1;
        if (Check(mid)) low=mid+1;
        else high=mid-1;
    }
    while (Check(low+1))    low++;
    while (!Check(low)) low--;
    printf("%d\n",low);
}

int main(){
    scanf("%d",&n);
    for (i=1;i<=n;i++)  scanf("%d%d",&x[i],&y[i]);
    Ready();    Work();
    return 0;
}
声明: 本文采用 BY-NC-SA 协议进行授权，如无注明均为原创，转载请注明转自 Marvolo
本文地址: 2-SAT学习笔记
2-SAT ACM 学习笔记
说点什么
登录
支持Markdown语法
好耶,沙发还空着ヾ(≧▽≦*)o
Loading...