已知有3种赛车和4种车道，其中三种普通车道可以通行两种赛车，一种特殊车道可以通行三种赛车。另有一些限制条件，格式为“若第i个车道通行p赛车，则j车道必须通行q赛车”。现求在满足所有限制条件的情况下，是否存在合法方案。

链接

BZOJ4945

LOJ2305

题解

如果考虑通行三种赛车的情况，则是一个3-SAT问题，该问题是NP-Hard的，不可做。

考虑到可以通行三种赛车的车道至多不超过8种，所以可以考虑强行对这些车道加上限制，使之变为普通车道。这样便转化成了一个2-SAT问题，可以顺利求解了。

中间有些细节需要注意，比如有些限制会强行指向不可通行的赛车种类，还有些限制是自相矛盾的。在枚举对特殊车道的限制时，需要考虑若有一条限制是指向该车道，且规定的赛车种类和车道类型相矛盾，需要将这种情况考虑为无解。具体细节参见代码。

输出方案时，需要比较两个分点的重标号的大小。标号小的即为选取的情况。

注：直接枚举车道类型，时间复杂度为O(3^d* n)，也就是下面的写法。理论上是不能通过的，需要排除一种情况将时间复杂度压到O(2^d* n)。下面的代码常数较小，所以才能顺利AC；但并不是正确的写法。

代码

#include<cstring>
#include<cstdio>
#include<iostream>
#include<algorithm>
#include<vector>
#include<cmath>
#include<queue>
#include<map>
#define N 100010
using namespace std;

int n,ss,m,i,cnt,dp,d;
int e[25];
int dfn[N],low[N],z[N],f[N],tag[N],op[N];
char c[N],C[N],Ans[N];

vector <int> r,son[N];

struct Data{
    int p,q;
    char x,y;
}t[N];

inline int Min(int a,int b){return (a<b)?a:b;}

inline int Get(int x,char y){
    if (C[x]=='a')  return (y=='B')?x+1:x+1+n;
    if (C[x]=='b')  return (y=='A')?x+1:x+1+n;
    if (C[x]=='c')  return (y=='A')?x+1:x+1+n;
}

inline void Ready(){
    int i=0;
    for (i=0;i<n;i++)
    if (c[i]=='x')  r.push_back(i);
    for (i=1;i<=n;i++)  op[i]=n+i,op[n+i]=i;
}

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 Print(){
    int i=0;
    for (i=1;i<=n;i++){
        if (C[i-1]=='a')    Ans[i]=(tag[i]<tag[i+n])?'B':'C';
        if (C[i-1]=='b')    Ans[i]=(tag[i]<tag[i+n])?'A':'C';
        if (C[i-1]=='c')    Ans[i]=(tag[i]<tag[i+n])?'A':'B';
    }
    for (i=1;i<=n;i++)  printf("%c",Ans[i]);
}

inline void Work(){
    int i=0,flag=0,a=0,b=0;
    while (!e[ss]){
        memcpy(C,c,sizeof(c));
        for (i=0;i<ss;i++)
            if (e[i]==0)    C[r[i]]='a';
            else if (e[i]==1)   C[r[i]]='b';
            else C[r[i]]='c';
        for (i=1;i<=2*n;i++)    son[i].clear();
        memset(dfn,0,sizeof(dfn));  memset(low,0,sizeof(low));
        memset(tag,0,sizeof(tag));  memset(z,0,sizeof(z));
        d=dp=cnt=0;
        for (i=1;i<=m;i++){
            if (C[t[i].p]-32==t[i].x)   continue;
            a=Get(t[i].p,t[i].x);   b=Get(t[i].q,t[i].y);
            if (C[t[i].q]-32==t[i].y){
                if (c[t[i].q]!='x') {
                    son[a].push_back(op[a]);    continue;
                }   else {
                    son[a].push_back(op[a]);    son[op[a]].push_back(a);
                }
            }
                else{
                son[a].push_back(b);    son[op[b]].push_back(op[a]);
            }
        }
        for (i=1;i<=2*n;i++)    if (!dfn[i])    Tarjan(i);
        flag=0;
        for (i=1;i<=n;i++)
            if (tag[i]==tag[i+n])   {
                flag=1; break;
            }
        if (!flag){
            Print();    exit(0);
        }
        e[0]++;
        for (i=0;i<ss;i++)  e[i+1]+=e[i]/3,e[i]%=3;
    }
}
int main(){
    scanf("%d%d",&n,&ss);
    scanf("%s",&c);
    scanf("%d",&m);
    for (i=1;i<=m;i++){
        scanf("%d",&t[i].p);    getchar();
        scanf("%c%d",&t[i].x,&t[i].q);  getchar();
        scanf("%c",&t[i].y);
        t[i].p--;   t[i].q--;
    }
    Ready();    Work();
    puts("-1");
    return 0;
}