【2-sat】2-sat算法内容及真题

A.2-sat简介

2-sat算法可以求解给定推出关系下的一种合法情况。题目中重常常，给定一些布尔变量A、B、C、D…，再给出一系列形如 $\longrightarrow A , C \longrightarrow \neg D$ 的推出关系，询问使得所有推出关系都成立的一组布尔变量取值。

B.2-sat算法内容

1.无解情况

一个变量要么为真，要么为假，不能同时为真又为假。
如果 $\longrightarrow \neg A$ ，那该变量不能取值为真，因为，为真就触发矛盾
如果 $\neg A \longrightarrow A$ ，那该变量不能取值为假，因为，为假就触发矛盾
所以，如果 $\longrightarrow \neg A$ ， $\neg A \longrightarrow A$ ，就找不到合法解。
其余情况有解。

2.构造合法解

尝试贪心地构造一组合法解。
观察这样一组情况
$\longrightarrow \neg B\longrightarrow C\longrightarrow \neg A\longrightarrow D \longrightarrow B$
由于关系的传递性，

如果A为真，后面5个变量都要合法，即 B为假，C为真，A为假，D为真，B为真。不难发现，A为真且为假，B为真且为假，矛盾。
如果A为假，只需最后3个变量合法，即D为真，B为真。

得出结论，对于变量A，选择拓扑序靠后一个，更优。具体一些，严格优于另一个。
推广到一般，对于任意变量X，选择拓扑序靠后的取值为答案中的值。

3.算法实现

首先，需要建图。假设共有n个变量，点 1,2,3…n表示变量为真情况，点 1 + n，2 + n，…n+n表示变量为假的情况。对于第 i 个变量，点 i 表示该变量为真，点 i + n表示该变量为假。往每个点中存入由该点能推出的点，例如，

变量 n 为真推出变量 1 为真，则往点n中存入1；
变量 n 为真推出变量 1 为假，则往点n中存入 1 + n；
变量 n 为假推出变量 1 为假，则往点n + n中存入 1

判断无解情况，对整个图求强联通分量，如果 i 与 i + n在一个强联通分量内部，则存在上文所说的 “ $\longrightarrow \neg A$ ， $\neg A \longrightarrow A$ ”，则无解。
如果有解，对每个变量，输出拓扑序靠后的一个，即强联通分量编号小的一个（tarjan算法的性质）。

\\tarjan
const int N = 1e6 + 10;
int dfn[N],low[N],cnt;
stack<int> stk;
bool ins[N];
int id[N],scc_cnt,sz[N];
vector<int> g[N];
int n,m;void tarjan(int u)
{dfn[u] = low[u] = cnt ++;stk.push(u);ins[u] = 1;for(auto j : g[u]){if(!dfn[j]){tarjan(j);low[u] = min(low[u],low[j]);}else if(ins[j]){low[u] = min(low[u],dfn[j]);}}if(dfn[u] == low[u]){int y;++scc_cnt;do{y = stk.top();stk.pop();ins[y] = 0;id[y] = scc_cnt;sz[scc_cnt] ++;}while(y != u);}
}

	\\判断有无解for(int i = 1; i <= 2*n; i ++){if(!dfn[i]) tarjan(i);}for(int i = 1; i <= n; i ++){if(id[i] == id[i+n]){cout << "NO\n";return;}}

	\\存储答案vector<int> ans;for(int i = 1; i <= n; i ++){if(id[i] < id[i + n])ans.push_back(i);}

例题 P4782 【模板】2-SAT

题目描述

有 $n$ 个布尔变量 $x_1\sim x_n$ ，另有 $m$ 个需要满足的条件，每个条件的形式都是「 $x_i$ 为 true / false 或 $x_j$ 为 true / false」。比如「 $x_1$ 为真或 $x_3$ 为假」、「 $x_7$ 为假或 $x_2$ 为假」。