Loj 2305 游戏

$2-SAT$ .

  • 如果没有地图 $x$ ,每张地图只能选两种车,就是个裸的 $2-SAT$ 问题.
  • 现在有地图 $x$ ,但不超过 $8$ 张.所以可以暴力枚举每张地图 $x$ 不能选哪种车,然后 $2-SAT$ 判断.
  • 注意枚举不能选的车时,只用枚举两种,就已经包含了地图 $x$ 选车的所有情况.
  • $2-SAT$ 问题若有解,输出一组合法解的方法,是对于每个状态 $i$ 与它的对立面 $inv(i)$ 比较所在 $scc$ 编号的大小,选择所在 $scc$ 编号小的状态.这样做是和缩点建反图后 $topsort$ 等价的.
  • 时间复杂度 $O(2^d\cdot (n+m))$ .
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
#include<bits/stdc++.h>
using namespace std;
typedef long long ll;
inline int read()
{
int out=0,fh=1;
char jp=getchar();
while ((jp>'9'||jp<'0')&&jp!='-')
jp=getchar();
if (jp=='-')
fh=-1,jp=getchar();
while (jp>='0'&&jp<='9')
out=out*10+jp-'0',jp=getchar();
return out*fh;
}
const int MAXN=3e5+10;
int n,m,d;
char buf[MAXN],s[10];
bool flag[MAXN];
int idx(int x,int type)
{
return x*3+type;
}
int inv(int id)
{
int x=id/3;
int t=id%3;
if(flag[idx(x,0)]==false)
return idx(x,3-0-t);
if(flag[idx(x,1)]==false)
return idx(x,3-1-t);
if(flag[idx(x,2)]==false)
return idx(x,3-2-t);
}
int ecnt=0,head[MAXN],to[MAXN],nx[MAXN];
void addedge(int u,int v)
{
++ecnt;
to[ecnt]=v;
nx[ecnt]=head[u];
head[u]=ecnt;
}
struct Edge
{
int x,y;
int hx,hy;
}E[MAXN];
int dfn[MAXN],low[MAXN],scc[MAXN],cnt,tot;
int stk[MAXN],tp,in[MAXN];
void tarjan(int u)
{
dfn[u]=low[u]=++cnt;
stk[++tp]=u;
in[u]=1;
for(int i=head[u];i;i=nx[i])
{
int v=to[i];
if(!flag[v])
continue;
if(!dfn[v])
{
tarjan(v);
low[u]=min(low[u],low[v]);
}
else if(in[v])
low[u]=min(low[u],dfn[v]);
}
if(dfn[u]==low[u])
{
int v;
++tot;
do
{
v=stk[tp--];
in[v]=0;
scc[v]=tot;
}while(u!=v);
}
}
bool solve(int st)
{
for(int i=0;i<n;++i)
{
if(buf[i]=='x')
{
int t=st&1;
flag[idx(i,0)]=true;
flag[idx(i,1)]=true;
flag[idx(i,t)]=false;
st>>=1;
}
}
memset(head,0,sizeof head);
ecnt=0;
for(int i=1;i<=m;++i)
{
int x=idx(E[i].x,E[i].hx);
int y=idx(E[i].y,E[i].hy);
if(x==y)
continue;
if(!flag[x])
continue;
else if(!flag[y])
addedge(x,inv(x));
else
{
addedge(x,y);
addedge(inv(y),inv(x));
}
}
memset(dfn,0,sizeof dfn);
memset(low,0,sizeof low);
memset(scc,0,sizeof scc);
memset(in,0,sizeof in);
tp=0;
tot=0;
cnt=0;
for(int i=0;i<3*n;++i)
if(flag[i] && !dfn[i])
tarjan(i);
for(int i=0;i<3*n;++i)
if(flag[i] && scc[i]==scc[inv(i)])
return false;
for(int i=0;i<3*n;++i)
{
if(flag[i] && scc[i]<scc[inv(i)])
putchar(i%3+'A');
}
puts("");
return true;
}
int main()
{
n=read(),d=read();
scanf("%s",buf);
for(int i=0;i<n;++i)
{
flag[idx(i,0)]=true;
flag[idx(i,1)]=true;
flag[idx(i,2)]=true;
if(buf[i]!='x')
flag[idx(i,buf[i]-'a')]=false;
}
m=read();
for(int i=1;i<=m;++i)
{
E[i].x=read()-1;
scanf("%s",s);
E[i].hx=s[0]-'A';
E[i].y=read()-1;
scanf("%s",s);
E[i].hy=s[0]-'A';
}
bool f=false;
for(int i=0;i<(1<<d);++i)
if(solve(i))
{
f=true;
break;
}
if(!f)
puts("-1");
return 0;
}