NOI2017-游戏-2sat
https://www.luogu.com.cn/problem/P3825
题意：有三种赛车A，B，C，以及用字符串 \(s\) 描述的地图，\(s_i=a/b/c\) 表示第 \(i\) 个地图不能用对应的 A/B/C 类型的赛车， \(s_i=x\) 表示可以选择任意一种，并且有 \(m\) 条限制，形如：若第 \(i\) 场选择了 \(h_i\) ，则 \(j\) 场要选择 \(h_j\) 。
同时保证了 \(s\) 中 "x" 的出现次数是 \(d\) ，\(1\leq |s|\leq 5\times 10^4,1\leq m\leq 10^5,0\leq d\leq 8\).
如果 \(s\) 中只有字母 \(a,b,c\) ，那么对于 \(s_i=a\) ，就只能选择 B 或 C，这是二选一并且要恰好选一个的，选B和选C是一对互斥的命题，加上 \(m\) 组关系形如“若 \(p\) 则 \(q\) ",2-sat的模型就呼之欲出了。当然这里在实现上有些细节：
- 如果 \(h_i = s_i\)，那么意味着若 \(p\) 则 \(q\) 这句话里，前提是一定不能选的（恒假），这个公式是恒真的，所以不用连边。
- 好了，那如果\(h_i\neq s_i\)，前提可能真可能假，那再看结论：
- 如果\(h_j=s_j\)，结论恒为假，2-sat其实不太允许我们在 \(x\) 和 \(\neg x\) 里添加第三种状态（这一点我没有严格证明过，但是一开始添加了一个叫做“恒假”的状态，wa了一片，不承认排中律的话好像会变成 3-sat 或者更困难的情况）。这种时候结论恒为假，为了保证”若 \(p\) 则 \(q\) “，那就一定要让 \(p\) 是假的，所以就连一条\(h_i\to \neg h_i\) 的边。
- 否则\(h_j\neq s_j\)，这时候就只要 \(h_i\to h_j\) 以及 \(\neg h_j\to \neg h_i\) 两条边。
好了现在有至多 \(8\) 个“x”，如果暴力枚举每个 "x" 取什么，那么有 \(3^8=6561\) 种状态，乘上 \(O(n+m)\) 大约有 \(10^9\)，太大了（至多 \(2m\) 条边和 \(2n\) 个点），然后就是这题另一个小转换，"x" 取 "a" 意味着能用 B或者C，取 “b” 意味着能用A或者C，这里就包含了 A、B、C的情况了，所以只要 $2^8=256 $ 地枚举就行了。
#include<bits/stdc++.h>
#define rep(i,a,b) for(int i=(a);i<=(b);i++)
#define fastio ios_base::sync_with_stdio(false);cin.tie(0);cout.tie(0)
using namespace std;
const int N=5e4+5;
const int M=1e5+5;
int n,d,m,bl[N<<1];
int a[M][2],idx[N][3],rev[N][3];
char ch[M][2],col[N<<1];
string s;
namespace SCC{
struct edge{
int to,nxt;
}edges[M<<1];
int head[N<<1],cnt;
int low[N<<1],dfn[N<<1],dfscnt,scc;
bool in_stack[N<<1];
stack<int> S;
void init(int _n){
dfscnt=scc=cnt=0;
rep(i,1,_n)low[i]=dfn[i]=head[i]=bl[i]=in_stack[i]=0;
}
void add(int u,int v){
edges[++cnt]=(edge){v,head[u]};
head[u]=cnt;
}
void tarjan(int x){
low[x]=dfn[x]=++dfscnt;
S.push(x);in_stack[x]=1;
for(int i=head[x];i;i=edges[i].nxt){
int to=edges[i].to;
if(!dfn[to]){
tarjan(to);
low[x]=min(low[x],low[to]);
}else if(in_stack[to])
low[x]=min(low[x],dfn[to]);
}
if(low[x]==dfn[x]){
++scc;
bool tag=0;
while(1){
bl[S.top()]=scc;
if(S.top()==x)tag=1;
in_stack[S.top()]=0;
S.pop();
if(tag)break;
}
}
}
};
void work(){
int mx=2*n;
SCC::init(mx);
rep(i,1,n){
rep(j,0,2)idx[i][j]=rev[i][j]=-1;
col[i]=((s[i-1]-'A'+1)%3+'A');
col[i+n]=((s[i-1]-'A'+2)%3+'A');
idx[i][col[i]-'A'] =i;
idx[i][col[i+n]-'A']=i+n;
rev[i][col[i]-'A'] =i+n;
rev[i][col[i+n]-'A']=i;
}
rep(tc,1,m){//2*m
int i=a[tc][0],j=a[tc][1];
char hi=ch[tc][0],hj=ch[tc][1];
if(hi!=s[i-1]){
if(hj==s[j-1]){
int u=idx[i][hi-'A'];
if(u<=n)SCC::add(u,u+n);
else SCC::add(u,u-n);
}else{
SCC::add(idx[i][hi-'A'],idx[j][hj-'A']);
SCC::add(rev[j][hj-'A'],rev[i][hi-'A']);
}
}
}
rep(i,1,mx)if(!bl[i])SCC::tarjan(i);
rep(i,1,n)if(bl[i]==bl[i+n])return;
rep(i,1,n){
if(bl[i]<bl[i+n])cout<<col[i];
else cout<<col[i+n];
}
exit(0);
}
int main(){
fastio;
cin>>n>>d>>s>>m;
rep(i,0,n-1)s[i]=s[i]-'a'+'A';
rep(i,1,m)cin>>a[i][0]>>ch[i][0]>>a[i][1]>>ch[i][1];
vector<int> pos;
rep(i,0,n-1)if(s[i]=='X')pos.push_back(i);
for(int S=0;S<(1<<d);S++){
rep(i,0,d-1){
if((S>>i)&1)s[pos[i]]='A';
else s[pos[i]]='B';
}
work();
}
cout<<-1;
return 0;
}