[NOI2017]游戏 （2sat)

https://www.cnblogs.com/cjyyb/p/8664527.html

#include<bits/stdc++.h>
using namespace std;
const int maxn=1e5+4;
int n,D,m,wm[maxn<<1],pos[maxn<<1],ch[maxn<<1],head[maxn<<1],cnt=0,dfn[maxn<<1],low[maxn<<1],vis[maxn<<1],tim=0,col[maxn<<1],sum=0;
struct node{
    int to,next;
}e[maxn<<1];
struct data{
    int x,y;
    char a,b;
}q[maxn<<1];
char g[maxn];
inline void add(int u,int v){
    e[cnt].to=v;e[cnt].next=head[u];head[u]=cnt++;
}
stack<int>s;
inline void tarjan(int u){
    dfn[u]=low[u]=++tim;
    vis[u]=1;
    s.push(u);
    for(int i=head[u];i!=-1;i=e[i].next){
        int v=e[i].to;
        if(!dfn[v]) {
            tarjan(v);
            low[u]=min(low[v],low[u]);
        }else if(vis[v]) low[u]=min(low[u],dfn[v]);
    }
    if(dfn[u]==low[u]){
        col[u]=++sum;
        vis[u]=0;
        while(!s.empty()){
            int x=s.top();s.pop();
            if(x==u) break;
            col[x]=sum;
            vis[x]=0;
        }
    }
}
inline void build(){
    for(int i=1;i<=m;i++){
        int x=q[i].x,y=q[i].y;
        int a=q[i].a-65,b=q[i].b-65;
        if(g[x]-97==a) continue;
        if(g[y]-97==b){
            if(wm[x]!=a){
                add(x+n,x);
            }else{
                add(x,x+n);
            }
            continue;
        }
        if(wm[x]==a){
            if(wm[y]==b){
                add(x,y);
                add(y+n,x+n);
            }else{
                add(x,y+n);
                add(y,x+n);
            }
        }else{
            if(wm[y]==b){
                add(x+n,y);
                add(y+n,x);
            }else{
                add(x+n,y+n);
                add(y,x);
            }
        }
    }
}
inline void calc(){
    memset(dfn,0,sizeof(dfn));
    memset(low,0,sizeof(low));
    memset(head,-1,sizeof(head));
    memset(col,0,sizeof(col));
    memset(e,0,sizeof(e));tim=0,sum=0,cnt=0;
    build();
    for(int i=1;i<=(n<<1);i++)
        if(!dfn[i]) tarjan(i);
    for(int i=1;i<=n;i++){
        if(col[i]==col[i+n]) return;
    }
    for(int i=1;i<=n;i++){
        if(g[i]=='a'){
            if(col[i]<col[i+n]) putchar('B');
            else putchar('C');
        }else if(g[i]=='b'){
            if(col[i]<col[i+n]) putchar('A');
            else putchar('C');
        }else{
            if(col[i]<col[i+n]) putchar('A');
            else putchar('B');
        }
    }
    exit(0);
}
inline void dfs(int k){
    if(k==D+1){
        calc();
        return;
    }
    g[pos[k]]='a';wm[pos[k]]=1;dfs(k+1);
    g[pos[k]]='b';wm[pos[k]]=0;dfs(k+1);
}
int main(){
    cin>>n>>D;D=0;
    scanf("%s",g+1);
    for(int i=1;i<=n;i++) {
        if(g[i]=='a') wm[i]=1,wm[i+n]=2;
        else if(g[i]=='b') wm[i]=0,wm[i+n]=2;
        else if(g[i]=='c') wm[i]=0,wm[i+n]=1;
        else wm[i+n]=2;
    }
    scanf("%d",&m);
    for(int i=1;i<=m;i++){
        scanf("%d %c%d %c",&q[i].x,&q[i].a,&q[i].y,&q[i].b);
    }
    for(int i=1;i<=n;i++) if(g[i]=='x') pos[++D]=i;
    dfs(1);
    cout<<-1;
}