[BZOJ4945][NOI2017]遊戲（2-SAT）

題目見http://www.lydsy.com/JudgeOnline/upload/Noi2017D2.pdf。

可以發現，除了x地圖之外，其餘的地圖隻适合兩種賽車。而在這裡，我們先假設所有的地圖都适合且隻适合兩種賽車，這樣就是 2−SAT 裸題了。

對于每場遊戲用兩個點 i 和i′，分别表示第 i 場遊戲使用該地圖适合的第一種賽車和第二種賽車（舉例：如果第i場遊戲的地圖不适合A賽車，那麼點 i 表示第i場遊戲使用B賽車，點 i′ 表示第 i 場遊戲使用C賽車）。

對于每個限制條件，設u為表示「第 i 場遊戲使用型号為hi的賽車」的點（在第 i 場遊戲的地圖适合型号為hi的賽車的情況下）， v 為表示「第j場遊戲使用型号為 hj 的賽車」的點（在第 j 場遊戲的地圖适合型号為hj的賽車的情況下），

那麼，

如果第 i 場遊戲的地圖不适合型号為hi的賽車，那麼不做任何操作。

如果第 i 場遊戲的地圖适合型号為hi的賽車，但第 j 場遊戲的地圖不适合型号為hj的賽車，那麼建邊 u−>u′ ，表示如果第 i 場遊戲使用了型号為hi的賽車則一定無解。

如果第 i 場遊戲的地圖适合型号為hi的賽車，第 j 場遊戲的地圖适合型号為hj的賽車，那麼建邊 u−>v ，表示如果第 i 場遊戲使用了型号為hi的賽車則第 j 場遊戲必須使用型号為hj的賽車，再建邊 v′−>u′ ，表示如果第 j 場遊戲不使用型号為hj的賽車則第 i 場遊戲不得使用型号為hi的賽車（逆否命題對稱）。

所有邊都建完之後跑一遍 Tarjan 強連通分量縮點。對于任意一個 i ，如果i和 i′ 在同一個強連通分量裡面，那麼此時無解。

否則輸出方案。 2−SAT 輸出方案的方法為：先把縮點之後的新圖進行拓撲排序，然後判斷每個點 i ，如果i所在強連通分量的拓撲序在 i′ 所在的強連通分量的拓撲序之後，那麼第 i 場遊戲使用該地圖适合的第一種賽車，否則使用第二種賽車。但是由于Tarjan求強連通分量就是按拓撲排序的逆序給出的，是以直接使用強連通分量編号判斷即可。即如果 bel[] 為每個點的所在強連通分量編号，那麼判斷為：如果 bel[i]<bel[i′] ，那麼使用該地圖适合的第一種賽車，否則使用第二種賽車。

現在考慮x地圖，考慮到隻有 8 張x地圖，如果假設它也隻适合兩種賽車，那麼暴力枚舉每個x地圖不适合賽車A或不适合賽車B（因為不适合賽車A就是适合賽車BC，不适合賽車B就是适合賽車AC，這樣就包含了ABC三種賽車），這樣每種地圖就都隻适合兩種賽車了。判斷時，如果已經枚舉遍了所有的2d種狀态都是無解，則原問題無解，否則輸出任意一種方案。

複雜度 O((n+m)∗2d) 。

代碼：

#include <cmath>
#include <cstdio>
#include <cstring>
#include <iostream>
#include <algorithm>
using namespace std;
inline int read() {
    int res = ; bool bo = ; char c;
    while (((c = getchar()) < '0' || c > '9') && c != '-');
    if (c == '-') bo = ; else res = c - ;
    while ((c = getchar()) >= '0' && c <= '9')
        res = (res << ) + (res << ) + (c - );
    return bo ? ~res +  : res;
}
inline char get() {
    char c; while ((c = getchar()) != 'A' && c != 'B' && c != 'C');
    return c;
}
const int N =  + ;
int n, d, m, a1[N], b1[N], ecnt, nxt[N], adj[N], go[N], dfn[N], low[N],
times, num, bel[N], top, stk[N], cyx[N];
char s[N], a2[N], b2[N], orz[N];
bool ins[N], flag;
void add_edge(int u, int v) {
    nxt[++ecnt] = adj[u]; adj[u] = ecnt; go[ecnt] = v;
}
int neg(int x) {return x > n ? x - n : x + n;}
int tran(int x, char c) {
    if (s[x] == 'a') return c == 'B' ? x : x + n;
    if (s[x] == 'b' || s[x] == 'c') return c == 'A' ? x : x + n;
    if (c == 'C') return x + n; return x;
}
void Tarjan(int u) {
    dfn[u] = low[u] = ++times; ins[stk[++top] = u] = ;
    for (int e = adj[u], v; e; e = nxt[e])
        if (!dfn[v = go[e]]) {
            Tarjan(v);
            low[u] = min(low[u], low[v]);
        }
        else if (ins[v]) low[u] = min(low[u], dfn[v]);
    if (dfn[u] == low[u]) {
        int v; bel[u] = ++num; ins[u] = ;
        while (v = stk[top--], v != u) bel[v] = num, ins[v] = ;
    }
}
bool solve() {
    int i; ecnt = times = num = ;
    for (i = ; i <= (n << ); i++) bel[i] = adj[i] = dfn[i] = ;
    for (i = ; i <= m; i++) if (s[a1[i]] != 'x' && s[b1[i]] != 'x') {
        if (a2[i] == s[a1[i]] - ) continue;
        int u = tran(a1[i], a2[i]), v;
        if (b2[i] == s[b1[i]] - ) {add_edge(u, neg(u)); continue;}
        v = tran(b1[i], b2[i]); add_edge(u, v);
        add_edge(neg(v), neg(u));
    }
    else {
        char o = s[a1[i]], p = s[b1[i]];
        int u, v, x = cyx[a1[i]], y = cyx[b1[i]];
        if (o == 'x' && p == 'x') {
            if (a2[i] == orz[x]) continue;
            u = tran(a1[i], a2[i]), v;
            if (b2[i] == orz[y]) {add_edge(u, neg(u)); continue;}
            v = tran(b1[i], b2[i]); add_edge(u, v);
            add_edge(neg(v), neg(u));
        }
        else if (o == 'x' && p != 'x') {
            if (a2[i] == orz[x]) continue;
            u = tran(a1[i], a2[i]), v;
            if (b2[i] == s[b1[i]] - ) {add_edge(u, neg(u)); continue;}
            v = tran(b1[i], b2[i]); add_edge(u, v);
            add_edge(neg(v), neg(u));
        }
        else {
            if (a2[i] == s[a1[i]] - ) continue;
            u = tran(a1[i], a2[i]), v;
            if (b2[i] == orz[y]) {add_edge(u, neg(u)); continue;}
            v = tran(b1[i], b2[i]); add_edge(u, v);
            add_edge(neg(v), neg(u));
        }
    }
    for (i = ; i <= (n << ); i++) if (!dfn[i]) Tarjan(i);
    for (i = ; i <= n; i++) if (bel[i] == bel[i + n]) return ;
    for (i = ; i <= n; i++) {
        if (bel[i] < bel[i + n]) {
            if (s[i] == 'a') putchar('B');
            else if (s[i] == 'b' || s[i] == 'C') putchar('A');
            else if (orz[cyx[i]] == 'A') putchar('B');
            else putchar('A');
        }
        else {
            if (s[i] == 'a' || s[i] == 'b') putchar('C');
            else if (s[i] == 'c') putchar('B');
            else if (orz[cyx[i]] == 'A') putchar('C');
            else putchar('B');
        }
    }
    return ;
}
void dfs(int dep) {
    if (dep > d) {
        if (!flag) flag = solve();
        if (flag) exit();
        return;
    }
    orz[dep] = 'A'; dfs(dep + );
    orz[dep] = 'B'; dfs(dep + );
}
int main() {
    int i; n = read(); read();
    scanf("%s", s + ); m = read();
    for (i = ; i <= n; i++) if (s[i] == 'x') cyx[i] = ++d;
    for (i = ; i <= m; i++) a1[i] = read(), a2[i] = get(),
        b1[i] = read(), b2[i] = get(); dfs();
    if (!flag) puts("-1");
    return ;
}