SAT 是适定性(Satisfiability)问题的简称。一般形式为 k - 适定性问题,简称 k-SAT。而当 \(k>2\) 时该问题为 NP 完全的。所以我们只研究 \(k=2\) 的情况。

——摘自 OI-Wiki

2-SAT问题大多是固定的模型:

给定若干个均有两个元素的集合,为了方便,我们称集合 \(i\) 中一个元素为 \(A_i\) ,另一个元素为 \(A_i'\) 。现在给出若干限制条件,如选择 \(A_i\) 就不能选择 \(A_j\) ,选择 \(A_i\) 就必须选择 \(A_j\) 等(其中 \(i \not= j\) )。询问是否存在一种方案,能够在满足限制条件的同时从每一个集合中都选出一个元素。

发现一个限制条件只和两个集合有关,于是我们可以考虑将这种关系抽象成图上的边,将集合中对立的两个元素抽象成点。

若现在有这样一个限制:选择 \(A_i\) 就不能选择 \(A_j\) 。那么如果选择 \(A_i\) 就必须选择 \(A_j'\) ,选择 \(A_j\) 就必须选择 \(A_i'\) 。对于这样的限制,连边 \(A_i \to A_j'\)\(A_j \to A_i'\) 。于是图中的边有了具体意义:\(u \to v\) 的边表示若选 \(u\) 则必选 \(v\)

不难发现,若一个点 \(u\) 被选择,则 \(u\) 所能到达的点均必须被选择。这个性质明显与连通性相关。

于是有了一个结论:若一个点 \(u\) 被选择,那么与 \(u\) 在同一个强连通分量中的点均必须被选择。

这句话说明同一个强连通分量中的点取或不取的状态是一致的

这样就能判断是否有解了:若同一个集合中的两个元素在同一个强连通分量中,则问题无解。很显然,若 \(A_i\)\(A_i'\) 要么同时选,要么都不选,则不满足题设。

求出强连通分量后判断无解:

for(int i=1;i<=n;++i)
	if(scc[i]==scc[i+n])
	{
		puts("IMPOSSIBLE");
		return 0;
    }

但是有些题不止让你判断有无解,还让你输出可行解,这就需要用到拓扑排序

\(S_i\) 表示 \(A_i\) 所在的强连通分量,\(S_i'\) 表示 \(A_i'\) 所在的强连通分量。

推广一下上面对于单点的结论:若一个强连通分量 \(S\) 被选择,则 \(S\) 所能到达的强连通分量均必须被选择

先考虑这样一种情况: \(S_i\)\(S_i'\) 联通,并且假设 \(S_i\) 的拓扑序小于 \(S_i'\) 的拓扑序。则必然有:若 \(S_i\) 被选择,则 \(S_i'\) 必须被选择。那肯定不能选 \(S_i\) 了,因为 \(S_i\)\(S_i'\) 必然不能同时选。这样我们就确定了选择方案。

\(S_i\)\(S_i'\) 不连通的话,上面的方法就不行了,因为没法确定选择方案,而一个看起来满足要求的方案可能会对其他的强连通分量产生影响,而枚举方案肯定复杂度爆炸。

我们尝试将两种情况进行统一,即选择 \(S_i\)\(S_i'\) 中拓扑序大的那个强连通分量。而这样选择其实是正确的,来简单证明一下:

由最初的连边方式可知,得出的图是对称的:

所以缩点后的DAG也是对称的:

考虑这么一个DAG:

不难看出 \(S_i'\) 的后继结点与 \(S_i\) 的前驱结点是对称的。

于是选择 \(S_i'\) 会导致 \(S_i'\) 的后继结点全部被选择,而选择 \(S_i'\) 就必须不选 \(S_i\) ,选择 \(S_i'\) 的后继结点会导致 \(S_i\) 的前驱结点不被选择。也就是说,\(S_i'\) 以下的结点全选, \(S_i\) 以上的结点全不选。不难看出,这样选择对虚线框中的结点无影响。

于是可知,这样选择不会导致矛盾。


跑完tarjan后不需要再拓扑,因为tarjan求出的scc编号就是逆拓扑序

注意一下:若将 \(i\) 集合拆成 i<<1i<<1|1 两个点,那么从2扫描到n<<1|1 求出的拓扑序对于第二种情况会出锅,大概是因为同一个连通块中结点的拓扑序不连续造成的。


\(\text{Code}:\)

#include <iostream>
#include <cstring>
#include <cstdio>
#include <algorithm>
#include <cmath>
#include <stack>
#define maxn 2000005
#define R register
#define INF 0x3f3f3f3f
using namespace std;
typedef long long lxl;

inline int read()
{
	int x=0,f=1;char ch=getchar();
	while(ch<'0'||ch>'9') {if(ch=='-') f=-1;ch=getchar();}
	while(ch>='0'&&ch<='9') {x=(x<<1)+(x<<3)+ch-'0';ch=getchar();}
	return x*f;
}

struct edge
{
	int u,v,next;
}e[maxn];

int head[maxn],k;

inline void add(int u,int v)
{
	e[k]=(edge){u,v,head[u]};
	head[u]=k++;
}

int n,m,ans[maxn];
int dfn[maxn],low[maxn],dfs_cnt,scc[maxn],scc_cnt;
std::stack<int> S;
bool vis[maxn];

inline void tarjan(int u)
{
	S.push(u);
	dfn[u]=low[u]=++dfs_cnt;
	for(int i=head[u];~i;i=e[i].next)
	{
		int v=e[i].v;
		if(!dfn[v])
		{
			tarjan(v);
			low[u]=min(low[u],low[v]);
		}
		else if(!scc[v]) low[u]=min(low[u],dfn[v]);
	}
	if(dfn[u]==low[u])
	{
		++scc_cnt;
		int x;
		do
		{
			x=S.top();S.pop();
			scc[x]=scc_cnt;
		} while (x!=u);
	}
}

int main()
{
	// freopen("P4782.in","r",stdin);
	n=read(),m=read();
	memset(head,-1,sizeof(head));
	for(int i=1;i<=m;++i)
	{
		int x=read(),a=read(),y=read(),b=read();
		add(x+n*(a&1),y+n*(b^1));
		add(y+n*(b&1),x+n*(a^1));
	}
	for(int i=1;i<=(n<<1);++i)
		if(!dfn[i]) tarjan(i);
	for(int i=1;i<=n;++i)
		if(scc[i]==scc[i+n])
		{
			puts("IMPOSSIBLE");
			return 0;
		}
	puts("POSSIBLE");
	for(int i=1;i<=n;++i)
		printf("%d ",scc[i]<scc[i+n]);
	return 0;
}

参考文献:国家集训队2003年论文集:伍昱--由对称性解2-SAT问题