2-SAT 问题与解法小结

这个算法十分的奇妙qwq... 将一类判定问题转换为图论问题，然后就很容易解决了。

本文有一些地方摘录了一下赵爽《2-SAT解法浅析》 （侵删）

一些概念

(SAT)问题：就是给一些布尔变量赋值，使得所有给你的条件成立的问题---适定性(Satisfiability)问题。我们令(k)为所有条件中含有变量的最大值，那么我们就可以称其为(k-SAT)问题。

可以证明(k>2)时候为NP完全问题，而(k=2)的时候存在多项式解法。

(2-SAT)问题 ： 就是对于每一个条件，最多只于两个变量的真假性有关，网上大部分博客都列出来了那11种条件，本文不再赘述（并且觉得没啥必要...）

基本建图方式

作为引入，我们在这里简单讨论一下其中一种情况。

(x lor y)也就是(x)为真或(y)为真的情况。

我们从这里可以得到两种情况：

1. (x)为假的时候，(y)必为真；
2. (y)为假的时候，(x)必为真。

我们把原图每个(x)拆成两个点，分别代表它为假和它为真。（习惯把他们标号为(2x)和(2x+1)。）

然后我们就可以得到(2x o 2y+1)和(2y o 2x+1)这两条边。

不难发现我们可以定义此处边的意义是“推导出” （来自刘汝佳的大白书）

对于其他的情况我们也都可以这样做。

例如：

1. (x)必为真，那么就可以连一条(2x o 2x+1)的边；
2. (x)为真时，(y)为假，那么就有一条(2x+1 o 2y)的边；
3. (x)和(y)状态要一样，(2x o 2y)和(2x + 1 o 2y + 1)的边。

但我们常常不能只连一条边，因为这样会出错（后文会提到）。

我们就可以引入另外一条边（也就是逆否命题等价）。

这从这个名称可以大概看出这条边是什么意思。

逆否命题等价：

如果我们有(x o y)的一个推导，那必定会有( eg y o eg x)的另一个推导。

也就是具有前一条边，就一定会有后一条边。

这是为什么呢qwq 我们可以通过之前那个例子2来简单说明一下。

(x)为真时，(y)为假，那么就有一条(2x+1 o 2y)的边

通过之前的定义，我们可以得到(2y+1 o 2x)的边。

也就是说(y)为真的时候，(x)必为假。（这个显然是要成立的）

之前举的第一个例子 强制使一个为真的状态 似乎就是两条边是一样的

所以整个图是个比较对称的一个图。

解法

有了上面那个图我们就很好办了！

如果我们会从(x)为真时候的状态推导出(x)为假的状态，那么肯定是不成立的。同样从假推到真也不行。

这个就是2-SAT不成立时候的情况。

那么我们先介绍一下解法一：

解法一：DFS枚举

我们首先枚举每个点的状态，真或者假（如果它之前没被标过）。然后将它能标记状态的全都标记一遍，

途中如果碰到自己这个状态已经被标记就返回真，如果反状态被标记了就返回假。

如果本状态当前假设状态不行，我们将它刚刚标出来的状态全部清空掉（用个栈来实现），

然后继续尝试它的一个反状态，如果反状态还是不行，那就是无解。

本算法没有回溯过程（可以yy一下证明。。。qwq）

最多尝试(n)个点，每次要最多尝试(m)条边，所以总复杂度是(mathcal O(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)这个状态当做答案，否则用它的反状态当做答案。

也就是我们用 sccno 小的状态当做答案。

代码实现

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; 

例题讲解

LA 3211(模板)

题意

给你一些飞机停靠的时间（每台飞机共两个时刻，早和晚）问你两个相邻飞机最小停靠间隔的最大值。

题解

模板题qwq 这种最小最大二分答案最好啦，然后用2-SAT去check一下。 （早为真，晚为假。然后两个状态无法共存的就连两条推导的边）

好像这个东西可以用线段树优化（h10的考试题）但我不会啊！！

LA 3713

题意

给你一些宇航员，按小于平均年龄和大于等于平均年龄分为两组，小于的只能执行(B)和(C)任务，大于等于的只能执行(A)和(C)任务。然后告诉你一些二元关系，就是代表哪对人不能分到同一组。问是否存在解，存在的话输出方案。

题解

虽然有三个任务，但每个人也是只有两个状态，也可以用2-SAT直接解决。也是不能共存的那种连边，手动模拟一下就好了。

ps : DFS可以直接过本题((n le 10^5))的数据.... 这就是我怀疑复杂度的起源...

【NOI2017】游戏

题意

见链接。。不想再写了。。

题解

NOI真题模拟！！！好像是第一次考2-SAT？

看我另外一篇博客题解就行咯qwq [UOJ317]【NOI2017】游戏 题解....