2-sat是什么

一类问题是这样的:

(两个符号的意思 $\lor \ or,\land \ and$)

有n个布尔变量,现在对它们做出限制,比如$a_i=1,a_i \lor a_j=1$,求一组可行的解。

假设限制元素最多的限制限制了k个元素,这个问题就被称为k-sat问题。

可以证明(然而我不会),$k>2$时是NPC的。

基础想法

把每个变量$a_i$拆成2个点$i_0,i_1$,表示它为1或0

每个变量就变成了一个集合。要求在每个集合里选一个元素,满足所有限制。

然后有向边$<u,v>$表示若选u则选v。

$a_i=1$型限制

连$<i_0,i_1>$。

$a_i=0$则反过来。

$a_i=a_j$限制

连$<i_0,j_0><j_0,i_0><i_1,j_1><j_1,i_1>$

$a_i\not=a_j$限制

连$<i_0,j_1><j_0,i_1><i_1,j_0><j_1,i_0>$

$a_i\lor a_j=1$或者$a_i\land a_j =0$限制

对于前者,连$<i_0,j_1><j_0,i_1>$

后者显然是交换0,1

$a_i\lor a_j=0$或者$a_i\land a_j =1$ 限制

拆开,转化为$a_i=1$型限制

其实都很显然是吧。

算法1

有一个很显然的结论:设$u'$表示u所在集合的另一个元素。

如果存在$<u,v>$则一定存在$<v',u'>$(对称性)

那么我们可以按照顺序枚举每一个布尔变量。

假设它是0,然后沿着单向边计算它影响的元素,如果没有问题就是0,并且计算它影响的元素的值。

否则假设它是1,如果没问题就是1,并且计算它影响元素的值。

否则无解。

由于对称性以及边是单向的,可以证明这个算法的正确性。(或者感性理解)

时间复杂度$O(nm)$其中n是点数m是边数。

当然0,1的顺序是可以交换的。

这个算法可以求出字典序最小的解。

在算之前,按照每个变量0,1编号较小值从小到大排序。

然后枚举要先枚举每个变量编号较小的那个点。

算法2

有没有更快的算法呢?

当然是有的。

我们可以先tarjan 强连通分量缩点。

那么同一个强连通分量里,点的选择情况是一样的(选则都选,不选则都不选)。

由对称性可知如果$u,v$在同一个强连通分量里,那么$u',v'$也在同一个强连通分量里。

如果$u,u'$在同一个强连通分量里,那么无解。

否则考虑,缩完点后得到了一个DAG,由两个边相反的DAG组成。

我们可以通过拓扑排序,每次找一个没有出边的分量,如果它里面点的对称点没有被选择,那么执行如下操作:

选择它里面的所有点。

把它扔掉。(把所有到它的边断掉)

可以发现是对的。

时间复杂度$O(n+m)$,通常用来计算可行解或者判断可行性。

算法3(黑科技)

不难发现,在缩完点后,如果u能到达v,那么在tarjan 中,u一定在v之后被找到。

于是我们可以在拓扑排序中,每次取能取的,编号最小的分量,

显然,如果一个分量$u$和分量$v$是对称的,那么如果$u<v$,会选择u,否则会选择v。

那么就不用重建图拓扑排序了。

常数优化/代码量优化效果还是很明显的。

例题

满汉全席

模板题。

NOI 2017 Day2T1 游戏

之所以用UOJ是因为ex test巨强无比。

发现有一些地图是X,3种都可以,但是个数不超过8.

我们可以把X转化为A或B。

枚举每个X转化为A还是B,跑2-SAT就可以了。

/*
Authlor: CNYALI_LK
LANG: C++
PROG: 317.cpp
Mail: cnyalilk@vip.qq.com
*/
#include<bits/stdc++.h>
#define debug(...) fprintf(stderr,__VA_ARGS__)
#define DEBUG printf("Passing [%s] in LINE %d\n",__FUNCTION__,__LINE__)
#define Debug debug("Passing [%s] in LINE %d\n",__FUNCTION__,__LINE__)
#define all(x) x.begin(),x.end()
using namespace std;
const double eps=1e-8;
const double pi=acos(-1.0);
typedef long long ll;
typedef pair<int,int> pii;
template<class T>int chkmin(T &a,T b){return a>b?a=b,1:0;}
template<class T>int chkmax(T &a,T b){return a<b?a=b,1:0;}
template<class T>T sqr(T a){return a*a;}
template<class T>T mmin(T a,T b){return a<b?a:b;}
template<class T>T mmax(T a,T b){return a>b?a:b;}
template<class T>T aabs(T a){return a<0?-a:a;}
#define min mmin
#define max mmax
#define abs aabs
int read(){
    int s=0,base=1;
    char c;
    while(!isdigit(c=getchar()))if(c=='-')base=-base;
    while(isdigit(c)){s=s*10+(c^48);c=getchar();}
    return s*base;
}
char rc(){
    char c;
    while(!isalpha(c=getchar()));
    return c;
}
void rs(char *s){
    while(!isalpha(*s=getchar()))++s;
    while(isalpha(*s))*(++s)=getchar();
    *s=0;
}
char WriteIntBuffer[1024];
template<class T>void write(T a,char end){
    int cnt=0,fu=1;
    if(a<0){putchar('-');fu=-1;}
    do{WriteIntBuffer[++cnt]=fu*(a%10)+'0';a/=10;}while(a);
    while(cnt){putchar(WriteIntBuffer[cnt]);--cnt;}
    putchar(end);
}
struct _limit{
    int a,b,ax,bx;
};
_limit a[102424];
char s[102424];
_limit limit(){
    _limit x;
    x.a=read()-1;
    x.ax=rc();
    x.b=read()-1;
    x.bx=rc();
    return x;
}
int h[102424];
int beg[102424],to[233333],lst[233333],dfn[102423],low[102423],no[102423]; 
int blocks,e,t;
void add(int u,int v){
    to[++e]=v;
    lst[e]=beg[u];
    beg[u]=e;
}
int stk[102424],*top=stk;
void dfs(int x){
    dfn[x]=low[x]=++t;
    *(++top)=x;
    flor(int i=beg[x];i;i=lst[i])
        if(dfn[to[i]]){
            if(!no[to[i]])
                chkmin(low[x],dfn[to[i]]);
        }else{
            dfs(to[i]);
            chkmin(low[x],low[to[i]]);
        }
    if(dfn[x]==low[x]){
        ++blocks;
        do{
            no[*(--top+1)]=blocks;
        }while(*(top+1)!=x);
    }
}

int main(){
#ifdef cnyali_lk
    freopen("317.in","r",stdin);
    freopen("317.out","w",stdout);
#endif
    int n,d,m;
    n=read();
    d=read();
    rs(s);
    int xs=0;
    flor(int i=0;i<n;++i){
        if(s[i]=='x'){h[xs]=i;++xs;}
    }
    m=read();
    flor(int i=1;i<=m;++i){
        a[i]=limit();
    }
    int un=1<<d,u,v;
    flor(int j=0;j<un;++j){
        flor(int i=0;i<d;++i)s[h[i]]='a'+!!(j&(1<<i));
        flor(int i=0;i<n+n;++i)beg[i]=dfn[i]=low[i]=no[i]=0;
        blocks=e=t=0;   
        flor(int i=1;i<=m;++i){
            if(a[i].ax-'A'==s[a[i].a]-'a')continue;
            if(a[i].bx-'A'==s[a[i].b]-'a'){
                int u=a[i].a*2+(a[i].ax-'A'-(a[i].ax-'A'>=s[a[i].a]-'a'));
                add(u,u^1);
            }
            else{
                int u=a[i].a*2+(a[i].ax-'A'-(a[i].ax-'A'>=s[a[i].a]-'a'));
                int v=a[i].b*2+(a[i].bx-'A'-(a[i].bx-'A'>=s[a[i].b]-'a'));
                add(u,v);
                add(v^1,u^1);
            }
        }
        flor(int i=0;i<n+n;++i)if(!dfn[i])dfs(i);
        int ok=1;
        flor(int i=0;i<n;++i)if(no[i<<1]==no[i<<1|1])ok=0;
        if(ok){
            flor(int i=0;i<n;++i){
                int ans=(no[i<<1]>no[i<<1|1]);
                ans+=(ans>=s[i]-'a');
                putchar(ans+'A');
            }
            return 0;
        }
    }
    printf("-1\n");
    return 0;
}

标签: 2-Sat

添加新评论