【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;
}