2-SAT 浅谈

P4782 【模板】2-SAT 问题

2-SAT 问题，描述类似存在多组关系，求解当所有关系成立时的情况，因为描述关系之间只存在可以互相推导和不能互相推导两种关系，所以称作 2-SAT 。

我们针对一个 \((a \lor b)\)（表示 \(a\) 和 \(b\) 其中有一个为真即成立）的状态，我们可以推导出两个二元对立的式子，为：\(\lnot a \to b \land \lnot b \to a\) 表示 \(a | b\) 其中一个为假时，另外一个一定为真，但相反其中一个为真时，不能推出另一个一定为真或假，所以我们可以说：\(\lnot a \to b \land \lnot b \to a\) 是 \((a \lor b)\) 的充要条件，但 $a \to b $ 是 \((a \lor b)\) 的充分条件，不能直接推导。

根据上述，我们发现如果按照 \(\lnot a \to b\) 表示 \(\lnot a\) 向 \(b\) 建一条边的方式来见图，我们可以得到一张有向有环图，具有性质，一个环内的点(条件)是可以相互推导的，环内，我们可以使用 tarjan 算法进行缩点。

不合理的情况：即环内的点不符逻辑( \(\lnot a\) 与 \(a\) 处在同一强连通分量)，一定是错误的。

如何构造合理方案？

缩点形成的一张 DAG 拓扑排序后，一个先出现的点抵达所有点一次构成的方案一定合理，所以我们枚举所有点，直接记录它先出现的方案，输出。

注意：tarjan 算法缩点后形成的 DAG 具有反拓扑序，即先出现的点是拓扑排序后出现的，正好与正序相反。

Code.

#include<bits/stdc++.h>
using namespace std;
const int N=2e6+10,M=4e6+10; 
int n,m,dfn[N],low[N],nowstep,idx,ne[M],e[M],stk[N],h[N],tt,scc_cnt,id[M];
bool in_stk[N];
void add(int u,int v) {ne[++idx]=h[u],e[idx]=v,h[u]=idx;}
void tarjan(int u)
{
	dfn[u]=low[u]=++nowstep,stk[++tt]=u,in_stk[u]=1;
	for(int i=h[u];~i;i=ne[i])
	{
		int j=e[i];
		if(! dfn[j])
		{
			tarjan(j);
			low[u]=min(low[u],low[j]);
		}
		else if(in_stk[j]) low[u]=min(low[u],dfn[j]);
	}
	if(low[u]==dfn[u])
	{
		int y; scc_cnt++;
		do
		{
			y=stk[tt--]; in_stk[y]=0;
			id[y]=scc_cnt;
		}while(y!=u);
	}
}
int main()
{
	memset(h,-1,sizeof h);
	scanf("%d%d",&n,&m);
	while(m--)
	{
		int x,a,y,b;
		scanf("%d%d%d%d",&x,&a,&y,&b);
		x--,y--;
		add(2*x+!a,2*y+b),add(2*y+!b,2*x+a);
	}
	for(int i=0;i<2*n;i++)
		if(!dfn[i]) tarjan(i);
	for(int i=0;i<n;i++)
		if(id[i*2]==id[i*2+1]) 
		{
			puts("IMPOSSIBLE");
			return 0;
		}
	puts("POSSIBLE");
	for(int i=0;i<n;i++)
		printf("%d ",(id[i*2]<id[i*2+1]) ? 0 : 1);
	return 0;
}

标签：tarjan,lnot,浅谈,int,stk,dfn,low,SAT
来源： https://www.cnblogs.com/EastPorridge/p/16412768.html