游戏「NOI2017」（2-SAT）

题目链接

Solution

别看这是道NOI的题，是到黑题，但其实它是道模板题。。。

其实这道题就是一个2-SAT+3-SAT。

虽然说3-SAT没有多项式复杂度的解法，但我们发现它最多会有d=8个3-SAT的格子，直接枚举即可。

注意枚举时只用枚举A，B两种即可因为A，B已经包含了全部三种情况。

然后这道题就变成普通的2-SAT问题了。

建图时i表示第i个格子选字典序小的车，i+n表示选字典序大的车。

如果要求中第一个要求第i个格子要选的车和这个格子的字母一样则不用管它。

如果第二个要求一样则可推出如果选第一个要求则不行，将第一个要求i连向i+n或i+n连向i。

剩下就是普通的2-SAT了。

Code

#include <iostream>
#include <cstdio>
#include <cstring>
using namespace std;
const int N = 100010;
const int M = 200010;
struct node{
    int pre, to;
    node() {
        pre = to = 0;
    }
    node(int _pre, int _to) {
        pre = _pre;
        to = _to;
    }
}edge[M];
int head[N], tot;
int n, d;
int m;
char s[N], t[N];
int a[M], b[M];
char h1[M], h2[M];
int dfn[N], low[N], stk[N], top, dep;
int col[N], scc;
bool vis[N];
int pos[10];
void add(int u, int v) {
    edge[++tot] = node(head[u], v);
    head[u] = tot;
}
void tarjan(int x) {
    dfn[x] = low[x] = ++dep;
    stk[++top] = x;
    vis[x] = 1;
    for (int i = head[x]; i; i = edge[i].pre) {
        int y = edge[i].to;
        if (!dfn[y]) {
            tarjan(y);
            low[x] = min(low[x], low[y]);
        } else if (vis[y]) {
            low[x] = min(low[x], dfn[y]);
        }
    }
    if (low[x] == dfn[x]) {
        scc++;
        vis[x] = 0;
        col[x] = scc;
        while (stk[top] != x) {
            col[stk[top]] = scc;
            vis[stk[top]] = 0;
            top--;
        }
        top--;
    }
}
void init() {
    top = dep = scc = 0;
    for (int i = 1; i <= n << 1; i++) {
        vis[i] = 0;
        dfn[i] = low[i] = col[i] = 0;
    }
    for (int i = 1; i <= n << 1; i++) head[i] = 0;
    tot = 0;
}
void work(int x) {
    for (int i = 1; i <= d; i++) {
        if ((x >> (i - 1)) & 1) {
            s[pos[i]] = 'A';
        } else {
            s[pos[i]] = 'B';
        }
    }
    for (int i = 1; i <= m; i++) {
        if (h1[i] == s[a[i]]) continue;
        if (h2[i] == s[b[i]]) {
            if (h1[i] == 'C' || (h1[i] == 'B' && s[a[i]] == 'C')) add(a[i] + n, a[i]);
            else add(a[i], a[i] + n);
        } else {
            int ad1, ad2;
            if (h1[i] == 'C' || (h1[i] == 'B' && s[a[i]] == 'C')) ad1 = 1;
            else ad1 = 0;
            if (h2[i] == 'C' || (h2[i] == 'B' && s[b[i]] == 'C')) ad2 = 1;
            else ad2 = 0;
            add(a[i] + n * ad1, b[i] + n * ad2);
            add(b[i] + n * (1 - ad2), a[i] + n * (1 - ad1));
        }
    }
}
bool check() {
    for (int i = 1; i <= n << 1; i++) {
        if (!dfn[i]) tarjan(i);
    }
    for (int i = 1; i <= n; i++) {
        if (col[i] == col[i + n]) return false;
    }
    return true;
}
int main() {
    scanf("%d%d", &n, &d);
    scanf("%s", s + 1);
    for (int i = 1, j = 0; i <= n; i++) {
        if (s[i] == 'x') {
            pos[++j] = i;
        }
        s[i] = s[i] - 'a' + 'A';
    }
    scanf("%d", &m);
    for (int i = 1; i <= m; i++) {
        scanf("%d %c %d %c", &a[i], &h1[i], &b[i], &h2[i]);
    }
    for (int state = 0; state < (1 << d); state++) {
        init();
        work(state);
        if (check()) {
            for (int i = 1; i <= n; i++) {
                if (col[i] < col[i + n]) {
                    if (s[i] == 'A') putchar('B');
                    else putchar('A');
                } else {
                    if (s[i] == 'C') putchar('B');
                    else putchar('C');
                }
            }
            return 0;
        }
    }
    puts("-1");
    return 0;
}