2-SAT学习笔记

2-SAT问题概念

给定一串布尔变量，每个变量只能为真或假。要求对这些变量进行赋值，满足布尔方程。这就是2-SAT问题。

求解2-SAT问题

• 构造状态

我们发现每块点都有两种状态（真、假），于是我们可以想到将点 \(u\)​​ 拆分成 \(u0,u1\)​ ，分别表示 \(u\)​ 点为假、真。我们若连的边为 \(u \to v\) ，就表示选择 \(u\) 就必须选 \(v\) 。

如果题目给出了一种条件 \(a \and b = true\)​​ ，那么我们就连一条 \(a1 \to b1\)​​ 的边。

连边方法：

1. \(a \and b = true \Rightarrow (a1,b1),(b1,a1)\)
2. \(a \and b = false \Rightarrow (a1,b0),(b1,a0)\)​
3. \(a \or b = true \Rightarrow (a0,b1),(b0,a1)\)​​
4. \(a \or b = false \Rightarrow (a0,b0),(b0,a0)\)​​

• 判断有无解

由所构造的状态可知，对于图中的每一个强连通分量，如果选择了其中任意一个点，那就意味着这个强连通分量中的所有点都要选。显然 \(x0,x1\)​​ 不可以同时选，由此可以判断有无解。

• 方案输出

由连边的方式可以得知，我们对于每个点的两种状态，选择拓扑序大的，舍弃掉另一个。

小技巧：这里可以不用再搞一遍拓扑排序，因为 \(Tarjan\)​ 求强连通分量每个点所在的强连通分量编号可以代替拓扑序。

如果要求字典序最小呢？用dfs枚举点 \(1 \to 2n\) ，如果这个点可以选，那就将与其相连的点都选上。如果发生冲突，就取消选择这个点以及与其相连的点。

P4782 【模板】2-SAT 问题

模板题，可以结合代码感性理解。

代码：

#include <stack>
#include <cstdio>
#include <vector>
#define min(a,b) ((a)<(b)?(a):(b))
using namespace std;
const int N=2e6+7;

vector<int> edge[N];

stack<int> sta;

int dfn[N],low[N];
int leader[N]; // 所属强连通分量编号

int n,m,deep,cnt;

inline void AddEdge(int u,int v) {
	edge[u].push_back(v);
}

inline void Tarjan(int u) {
	dfn[u]=low[u]=++deep;
	sta.push(u);
	for(int i=0,v;i<edge[u].size();++i) {
		v=edge[u][i];
		if(!dfn[v]) {
			Tarjan(v);
			low[u]=min(low[u],low[v]);
		}
		else if(!leader[v])
			low[u]=min(low[u],dfn[v]);
	}
	if(dfn[u]==low[u]) {
		++cnt;
		while(sta.top()!=u) {
			leader[sta.top()]=cnt;
			sta.pop();
		}
		leader[sta.top()]=cnt;
		sta.pop();
	}
}

signed main() {
	scanf("%d%d",&n,&m);
	for(int a,x,b,y;m;--m) {
		scanf("%d%d%d%d",&a,&x,&b,&y);
		if(!x && !y)
			AddEdge(a+n,b),AddEdge(b+n,a);
		else if(x && y)
			AddEdge(a,b+n),AddEdge(b,a+n);
		else if(!x && y)
			AddEdge(b,a),AddEdge(a+n,b+n);
		else  if(x && !y)
			AddEdge(a,b),AddEdge(b+n,a+n); // a表示a0,a+n表示a1
	}
	for(int i=1;i<=(n<<1);++i)
		if(!dfn[i])
			Tarjan(i); // 使用强连通分量求解
	for(int i=1;i<=n;++i)
		if(leader[i]==leader[i+n]) // 若a0和a1必须同时选,就无解
			return puts("IMPOSSIBLE"),0;
	puts("POSSIBLE");
	for(int i=1;i<=n;++i)
		printf("%d ",leader[i]>leader[i+n]); // 输出一组解
    return 0;
}

标签：a1,int,笔记,学习,a0,b0,b1,SAT
来源： https://www.cnblogs.com/wshcl/p/2-SAT.html