本文介绍了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;
}