题解：
一眼看过去还以为是3-sat
其实d只有8
那么我们可以枚举每一个x选择哪一个
然后再用2-sat处理
代码：
#include<bits/stdc++.h> using namespace std; const int N=100005,M=N<<6,ABC='A'+'B'+'C'; struct Edge{int to,next;}e[M]; int n,m,K,pos[10],zz[M],ne[M],mi[N],mj[N],fi[N<<1],len,st[N],cot; char Str[N],hi[N],hj[N];bool Mark[N<<1],Un[N<<1]; void jb(int x,int y) { zz[++len]=y;ne[len]=fi[x];fi[x]=len; zz[++len]=x^1;ne[len]=fi[y^1],fi[y^1]=len; } int dfs(int x) { if (Mark[x^1]||(n>10000&&Un[x]))return 0; if (Mark[x])return 1; Mark[x]=1;st[++cot]=x; for (int i=fi[x];i;i=ne[i]) if (!dfs(zz[i])) { Un[x]=1; return 0; } return 1; } void init() { memset(fi,0,sizeof fi); memset(Mark,0,sizeof Mark); memset(Un,0,sizeof Un); } int pd() { len=1;int n1,n2; init(); for (int i=1;i<=m;i++) { if (hi[i]==Str[mi[i]])continue; n1=hi[i]>ABC-hi[i]-Str[mi[i]]; if (hj[i]==Str[mj[i]])jb(mi[i]<<1|n1,mi[i]<<1|n1^1); else n2=hj[i]>ABC-hj[i]-Str[mj[i]],jb(mi[i]<<1|n1,mj[i]<<1|n2); } for (int i=1;i<=n;i++) { cot=0; if (!dfs(i<<1)) { while (cot)Mark[st[cot--]]=0; if (!dfs(i<<1|1))return 0; } } for (int i=1;i<=n;i++) if (Mark[i<<1])putchar(Str[i]=='A'?'B':'A'); else putchar(Str[i]=='C'?'B':'C'); return 1; } int main() { scanf("%d%d%s%d",&n,&K,Str+1,&m); int cnt=0; for (int i=1;i<=m;i++)scanf("%d%s%d%s",&mi[i],&hi[i],&mj[i],&hj[i]); for (int i=1;i<=n;i++) if (Str[i]=='x')pos[cnt++]=i;else Str[i]+='A'-'a'; for (int i=0;i<1<<K;i++) { for (int j=0;j<K;j++)Str[pos[j]]='A'+(i>>j&1); if (pd())return 0; } puts("-1"); return 0; }