2-SAT 问题与解法小结
这个算法十分的奇妙qwq... 将一类判定问题转换为图论问题，然后就很容易解决了。
本文有一些地方摘录了一下赵爽《2-SAT解法浅析》 （侵删）
- 一些概念：
\(SAT\)问题：就是给一些布尔变量赋值，使得所有给你的条件成立的问题---适定性(Satisfiability)问题。我们令\(k\)为所有条件中含有变量的最大值，那么我们就可以称其为\(k-SAT\)问题。
可以证明\(k>2\)时候为NP完全问题，而\(k=2\)的时候存在多项式解法。
\(2-SAT\)问题 ： 就是对于每一个条件，最多只于两个变量的真假性有关，网上大部分博客都列出来了那11种条件，本文不再赘述（并且觉得没啥必要...）
- 基本建图方式：
作为引入，我们在这里简单讨论一下其中一种情况。
\(x \lor y\)也就是\(x\)为真或\(y\)为真的情况。
我们从这里可以得到两种情况：
- \(x\)为假的时候，\(y\)必为真；
- \(y\)为假的时候，\(x\)必为真。
我们把原图每个\(x\)拆成两个点，分别代表它为假和它为真。（习惯把他们标号为\(2x\)和\(2x+1\)。）
然后我们就可以得到\(2x+1\to y\)和\(2y+1 \to x\)这两条边。
不难发现我们可以定义此处边的意义是“推导出” （来自刘汝佳的大白书）
对于其他的情况我们也都可以这样做。
例如：
- \(x\)必为真，那么就可以连一条\(2x+1 \to 2x+1\)的边；
- \(x\)为真时，\(y\)为假，那么就有一条\(2x+1 \to 2y\)的边；
- \(x\)和\(y\)状态要一样，\(2x \to 2y\)和\(2x + 1 \to 2y + 1\)的边。
但我们常常不能只连一条边，因为这样会出错（后文会提到）。
我们就可以引入另外一条边（也就是逆否命题等价）。
这从这个名称可以大概看出这条边是什么意思。
逆否命题等价：
如果我们有\(x \to y\)的一个推导，那必定会有\(\neg y \to \neg x\)的另一个推导。
也就是具有前一条边，就一定会有后一条边。
这是为什么呢qwq 我们可以通过之前那个例子2来简单说明一下。
- \(x\)为真时，\(y\)为假，那么就有一条\(2x+1 \to 2y\)的边
通过之前的定义，我们可以得到\(2y+1 \to 2x\)的边。
也就是说\(y\)为真的时候，\(x\)必为假。（这个显然是要成立的）
所以整个图是个比较对称的一个图。
- 解法：
有了上面那个图我们就很好办了！
如果我们会从\(x\)为真时候的状态推导出\(x\)为假的状态，那么肯定是不成立的。同样从假推到真也不行。
这个就是2-SAT不成立时候的情况。
那么我们先介绍一下解法一：
解法一：DFS枚举
我们首先枚举每个点的状态，真或者假（如果它之前没被标过）。然后将它能标记状态的全都标记一遍，
途中如果碰到自己这个状态已经被标记就返回真，如果反状态被标记了就返回假。
如果本状态当前假设状态不行，我们将它刚刚标出来的状态全部清空掉（用个栈来实现），
然后继续尝试它的一个反状态，如果反状态还是不行，那就是无解。
本算法没有回溯过程（可以yy一下证明。。。qwq）
最多尝试\(n\)个点，每次要最多尝试\(m\)条边，所以总复杂度是\(\Theta(nm)\)的。
（一开始我不相信这个复杂度...然后直到我碰到了真正的强数据...QAQ）
但其实它的表现是很优秀的，随机数据能很快的构造出解，并且比较好写，而且能求字典序最小的解。
还有一点，如果不连上之前的那个逆反命题等价，就会导致整个出错，就是你无法从后面状态反推回去原来的状态，然后就会导致一些本来可以成立的无法成立了。
ps : 我一开始错了，但顺着跑一遍，反着再跑一遍，似乎就可以了（也许是因为图是对称的？）
这个输出直接用
mark数组就行了，很简单。代码实现：
struct Two_SAT { bitset<N> mark; int Next[N], Head[N], to[N], e, n; void Init(int n) { this -> n = n; mark.reset(); Set(Head, 0); e = 0; } void add_edge(int u, int v) { to[++ e] = v; Next[e] = Head[u]; Head[u] = e; } void Add(int x, int xv, int y, int yv) { x = x << 1 | xv; y = y << 1 | yv; add_edge(x, y); add_edge(y ^ 1, x ^ 1); } //(x,xv) -> (y,yv) int sta[N], top; bool Dfs(int x) { if (mark[x ^ 1]) return false; if (mark[x]) return true; sta[++ top] = x; mark[x] = true; for (int i = Head[x]; i; i = Next[i]) if (!Dfs(to[i])) return false; return true; } bool Solve() { for (int i = 2; i <= 2 * n; i += 2) if (!mark[i] && !mark[i ^ 1]) { top = 0; if (!Dfs(i)) { while (top) mark[sta[top --]] = false; if (!Dfs(i ^ 1)) { return false; } } } return true; } } T; inline void Out() { For (i, 1, n) For (j, 0, 1) if (T.mark[i << 1 | j]) printf ("%d ", opt[i][j]); }解法二：Tarjan缩点+拓扑序
这个就是将原图用Tarjan缩点，然后再进行判断的。（对于缩点，参考我这篇博客【模板】缩点）
其实那篇只讲了代码实现，并没有讲为啥那样做，其实我也不知道如果对于一个点\(x?\)的两个状态真或假都在一个强联通分量（scc）中，那么肯定不成立。
我们可以用之前的那个DFS来配合理解，就是真能推导假，假也能推导到真，所以都不成立。
然后我们可以用拓扑序来染色求解，对于一个并未染色的点我们将它染成\(1\)，它的一个对立状态染成\(2\)。
然后不断重复。最后所有为\(1\)的就可以当做一组解了。
这个成立时因为，每个条件都是两两关系，只要保证了存在解，那么你这样绝对是可行的
（也可以理解为一连串的推导了）证明还是看那篇论文吧。。。
但写个拓扑序有点麻烦了。。我们可以利用Tarjan的一个性质，就是它的访问其实是根据拓扑序来的。
所以最后给他的scc标号（
sccno）正好和拓扑序相反。如果对于一个\(x\)
sccno比它的反状态\(x \wedge 1\)的sccno要大，那么我们用\(x\)这个状态当做答案，否则用它的反状态当做答案。代码实现：
struct Two_SAT {
int Next[N], Head[N], to[N], e, n;
void Init(int n) { this -> n = n; For(i, 2, n << 1 | 1) Head[i] = 0; e = 0; }
void add_edge(int u, int v) { to[++ e] = v; Next[e] = Head[u]; Head[u] = e; }
void Add(int x, int xv, int y, int yv) {
x = x << 1 | xv;
y = y << 1 | yv;
add_edge(x, y);
add_edge(y ^ 1, x ^ 1);
} //(x,xv) -> (y,yv)
int sccno[N], scc_cnt;
int dfn[N], lowlink[N];
int sta[N], top, clk;
void Tarjan(int u) {
lowlink[u] = dfn[u] = ++clk; sta[++ top] = u;
for (int i = Head[u]; i; i = Next[i]) {
int v = to[i];
if (!dfn[v]) { Tarjan(v); chkmin(lowlink[u], lowlink[v]); }
else if (!sccno[v]) chkmin(lowlink[u], dfn[v]);
}
if (lowlink[u] == dfn[u]) {
++ scc_cnt;
for (;;) {
int now = sta[top --];
sccno[now] = scc_cnt;
if (now == u) break ;
}
}
}
bool Solve() {
For (i, 2, n << 1 | 1) dfn[i] = sccno[i] = 0; scc_cnt = clk = 0;
For (i, 2, n << 1 | 1) if (!dfn[i]) Tarjan(i);
For (i, 1, n)
if (sccno[i << 1] == sccno[i << 1 | 1]) return false;
return true;
}
void Out() {
For (i, 1, n) { printf("%d ", opt[i][sccno[i << 1] > sccno[i << 1 | 1]]) ; }
}
} T;
一些简单的例题：
-
题意：给你一些飞机停靠的时间（每台飞机共两个时刻，早和晚）问你两个相邻飞机最小停靠间隔的最大值。
题解：模板题qwq 这种最小最大二分答案最好啦，然后用2-SAT去check一下。
（早为真，晚为假。然后两个状态无法共存的就连两条推导的边）
好像这个东西可以用线段树优化（h10的考试题）但我不会啊！！
-
题意：给你一些宇航员，按小于平均年龄和大于等于平均年龄分为两组，小于的只能执行\(B\)和\(C\)任务，大于等于的只能执行\(A\)和\(C\)任务。然后告诉你一些二元关系，就是代表哪对人不能分到同一组。问是否存在解，存在的话输出方案。
题解：虽然有三个任务，但每个人也是只有两个状态，也可以用2-SAT直接解决。也是不能共存的那种连边，手动模拟一下就好了。
ps : DFS可以直接过本题(\(n \le 10^5\))的数据.... 这就是我怀疑复杂度的起源...
