【NOI2017】游戏与2-sat方案输出

本文介绍了2-SAT输出一种方案的方法与证明,以及一种 $ O(nm) $ 复杂度输出最小字典序的方法.

2-SAT输出一种方案

先判定是否有解,缩点后得到一张DAG.对于命题组 $ (i,i') $ ,我们选择 $ i $ 和 $ i' $ 中拓朴序靠后的一个即可.

同时由于Tarjan缩点时本来就是拓朴序倒序缩点的,只需要选择 $ i $ 和 $ i' $ 中所属强连通分量中编号小的那个即可.

下面证明这种方案的正确性.我们使用反证法.

假如这样的做法不对,也就是说,会存在一条边 $ (u,v) $ ,使得命题 $ u $ 为 $ true $ 而命题 $ v $ 为 $ false $ .

因为命题 $ u $ 为 $ true $ ,我们得到命题 $ u' $ 的拓扑序在命题 $ u $ 之前.因为存在边 $ (u,v) $ ,我们得到命题 $ u $ 的拓扑序在命题 $ v $ 之前.而2-SAT问题具有对称性,即逆否命题之间真假性相同.如果选 $ u $ 则必须选 $ v $ ,反过来如果不选 $ v $ 则一定不能选 $ u $ ,所以就存在边 $ (v',u') $ ,从而拓扑序的顺序应该是 $ (v',u',u,v) $ , 那么 $ v $ 的拓扑序在 $ v' $ 之后,这与 $ v $ 为 $ false $ 矛盾.

2-SAT字典序最小方案

从一号点开始,先强制它为 $ true $ ,如果无解再强制它为 $ false $ ,一个一个确定下去即可.

NOI2017 游戏

题意

有三种赛车 $ A $ , $ B $ , $ C $ 和四种地图 $ a $ , $ b $ , $ c $ , $ x $ .地图 $ a/b/c $ 表示不能用赛车 $ A/B/C $ ,地图 $ x $ 可以用任意赛车.现有 $ n $ 张地图和 $ m $ 个限制,第 $ i $ 个限制形如:如果图 $ x $ 选择了赛车 $ u $ ,那么图 $ y $ 就必须选择赛车 $ v $ .要求判定是否有解,有解输出任意一种方案.

数据范围:设 $ x $ 型地图有 $ d $ 张, $ n,m≤100000,d≤8 $

题解

$ x $ 型地图可以看做在 $ a $ 型地图和 $ b $ 型地图中任选一个, $ 2^d $ 枚举一下.

剩下的就是直接 $ 2-SAT $ 跑一下输出方案.

注意命题和它的逆否命题要同时加入.

#pragma GCC optimize("2,Ofast,inline")
#define fi first
#define se second
#define LL long long
#define pb push_back
#define mp make_pair
#define pii pair<int, int>
#include<bits/stdc++.h>
using namespace std;
const int N = 3e5 + 10;
const int mod = 1e9 + 7;

template <typename T> void read(T &x) {
	int f = 0;
	register char c = getchar();
	while (c < '0' || c > '9') f |= (c == '-'), c = getchar();
	for (x = 0; c >= '0' && c <= '9'; c = getchar())
		x = (x << 3) + (x << 1) + (c ^ '0');
	if (f) x = -x;
}

int n, m, d, E, V;
int a[N], b[N], s[N];
int u[N], v[N];
char S[N];
int fir[N], nex[N << 1], arr[N << 1], num[N][3];
int tim, sccn, scc[N], low[N], dfn[N];
stack<int> st;

inline void Add_Edge(int x, int y) {
	nex[++E] = fir[x];
	fir[x] = E; arr[E] = y;
}

void dfs(int x) {
	dfn[x] = low[x] = ++tim;
	st.push(x);
	for (int i = fir[x]; i; i = nex[i]) {
		if (!dfn[arr[i]]) {
			dfs(arr[i]);
			low[x] = min(low[x], low[arr[i]]);
		}
		else if (!scc[arr[i]]) low[x] = min(low[x], dfn[arr[i]]);
	}
	if (low[x] == dfn[x]) {
		int y;
		++sccn;
		do {
			y = st.top();
			scc[y] = sccn;
			st.pop();
		} while (y != x);
	}
}

void check() {
	memset(fir, 0, sizeof(int) * (V + 1));
	memset(dfn, 0 ,sizeof(int) * (V + 1));
	memset(scc, 0, sizeof(int) * (V + 1));
	V = E = 1;
	for (int i = 1; i <= n; ++i) {
		for (int j = 0; j < 3; ++j) {
			num[i][j] = 0;
			if (s[i] != j) num[i][j] = ++V;
		}
	}
	for (int i = 1; i <= m; ++i) {
		if (!num[a[i]][u[i]]) continue;
		if (!num[b[i]][v[i]]) {
			int o = -1;
			for (int j = 0; j < 3; ++j) {
				if (j != u[i] && num[a[i]][j]) {
					o = j;
				}
			}
			Add_Edge(num[a[i]][u[i]], num[a[i]][o]);
			Add_Edge(num[a[i]][o] ^ 1, num[a[i]][u[i]] ^ 1);
		}
		else {
			Add_Edge(num[a[i]][u[i]], num[b[i]][v[i]]);
			Add_Edge(num[b[i]][v[i]] ^ 1, num[a[i]][u[i]] ^ 1);
		}
	}
	sccn = tim = 0;
	for (int i = 1; i <= V; ++i) {
		if (!dfn[i]) dfs(i);
	}
	for (int i = 1; i <= n; ++i) {
		if (scc[num[i][0]] == scc[num[i][1]]) return;
		if (scc[num[i][1]] == scc[num[i][2]]) return;
		if (scc[num[i][0]] == scc[num[i][2]]) return;
	}
	for (int i = 1; i <= n; ++i) {
		int u, v;
		if (s[i] == 0) u = 1, v = 2;
		if (s[i] == 1) u = 0, v = 2;
		if (s[i] == 2) u = 0, v = 1;
		printf("%c", scc[num[i][u]] < scc[num[i][v]] ? u + 'A' : v + 'A');
	}
	puts("");
	exit(0);
}

void Dfs(int x) {
	if (x == n + 1) return (void) (check());
	if (s[x] != -1) Dfs(x + 1);
	else {
		s[x] = 0;
		Dfs(x + 1);
		s[x] = 1;
		Dfs(x + 1);
		s[x] = -1;
	}
}

int main() {
	read(n); read(d);
	scanf("%s", S + 1);
	for (int i = 1; i <= n; ++i) {
		s[i] = (S[i] <= 'c') ? S[i] - 'a' : -1;
	}
	read(m);
	for (int i = 1; i <= m; ++i) {
		char x, y;
		scanf("%d %c %d %c", &a[i], &x, &b[i], &y);
		u[i] = x - 'A';
		v[i] = y - 'A';
	}
	Dfs(1);
	puts("-1");
	return 0;
}