2-SAT 问题与解法小结

Posted 2020-10-27 zjp_shadow

tags:

篇首语：本文由小常识网(cha138.com)小编为大家整理，主要介绍了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 \\to 2y+1\\)和\\(2y \\to 2x+1\\)这两条边。

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

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

例如：

\\(x\\)必为真，那么就可以连一条\\(2x \\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\\)条边，所以总复杂度是\\(\\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;