2-sat

k-sat

sat 是 Satisfiability 的缩写，就是对一串 bool 量进行赋值，使其满足布尔方程
具体来说，k-sat 就是给出若干个限制：

[a_{p_1}oplus a_{p_2}oplus cdotsoplus a_{p_k}=x ]

求的一组满足所有限制合法解，oplus$ 是一种二进制位运算，(a_pi) 是二进制数
若 (k>2)，可以证明是 NP 完全的，只能暴力做，所以更多的是讨论 (k=2) 的情况，也就是 2-sat，也就是每个限制只有两个未知数在其中

2-sat

P4782 【模板】2-SAT 问题

这个题的的每条限制是：

• (x_{p_1}lor x_{p_2}=1)
• (lnot x_{p_1}lor x_{p_2}=1)
• (lnot x_{p_1}lor lnot x_{p_2}=1)

其中之一，当然也有 (x_{p_1}lor lnot x_{p_2})，但是和第二种其实是一样的
用图论的方式解决，对于每个未知数拆成两个点，每个点分别代表 (x) 和 (lnot x)，就是 (x) 分别取真和假
然后尝试对于每一个限制，都用有向边表示出来，所以可以让边 ((a,b)) 来表示，如果 (a) 成立，则 (b) 一定也成立
比如 (a) 表示的是 (lnot x)，(b) 表示 (y)，意思就是，如果 (lnot x) 是成立的，根据限制条件，一定可以推导出 (y) 成立

考虑对于每一种条件如何连边

• (a lor bRightarrow (lnot a,b),(lnot b,a))
• (lnot alor bRightarrow (a,b),(lnot b,lnot a))
• (lnot alor lnot bRightarrow (a,lnot b),(b,lnot a))

而一个强连通分量中，每两个点都可以互相到达，“互相到达”在这里的意义就是，互为条件能使对方成立
那么，在一个强连通分量中，显然只要有一个点表示的信息是成立的，那么就可以推出整个强连通分量中所有点，所表示的信息都是成立的
就是“要么都成立，要么都不成立”

对于任意点 (x) 和 (lnot x)，限制条件有解，等价于存在一种符合构建的图上边的信息的选点方案（选一个点，指的就是让这个点表示的信息成立），使得这两个点有且只有一个成立
那么，如果存在一对 (x) 和 (lnot x) 在一个强连通分量中，就无解了，否则，一定有解

那么如何构造出一组可行解？
考虑一对 (x) 和 (lnot x)
tarjan 所点后的图是个 DAG，DAG 上拓扑序靠前的点，如果信息成立，就会影响到后面的点，使得后面点的信息也成立
所以，我们应该选择 (x) 和 (lnot x) 中拓扑序较大的点，让它的信息成立
而 tarjan 缩点时的，为每个强连通分量标记的编号，实际上是与拓扑序相反的，模拟一下小数据就能知道，它是从后往前出栈并标记
所以判断的时候是选择强连通分量标号小的点，让他的信息成立

代码中，用 (x+n) 表示 (lnot x)

其实 2-sat 的题难处就在于如何选择恰当的信息作为一个点，然后考虑如何连边，才能使这些点的信息成立或不成立都能确定下来

#include<cstdio>
#include<algorithm>
#include<iostream>
#include<cmath>
#include<map>
#include<iomanip>
#include<cstring>
#define reg register
#define EN std::puts("")
#define LL long long
inline int read(){
	register int x=0;register int y=1;
	register char c=std::getchar();
	while(c<'0'||c>'9'){if(c=='-') y=0;c=std::getchar();}
	while(c>='0'&&c<='9'){x=x*10+(c^48);c=std::getchar();}
	return y?x:-x;
}
#define N 2000006
#define M 2000006
int n,m;
struct graph{
	int fir[N],nex[M],to[M],tot;
	inline void add(int u,int v){
		to[++tot]=v;
		nex[tot]=fir[u];fir[u]=tot;
	}
}G;
int low[N],dfn[N],dfscnt;
int stack[N],top,scc[N],scccnt;
void tarjan(int u){
	low[u]=dfn[u]=++dfscnt;
	stack[top++]=u;
	for(reg int v,i=G.fir[u];i;i=G.nex[i]){
		v=G.to[i];
		if(!dfn[v]) tarjan(v),low[u]=std::min(low[u],low[v]);
		else if(!scc[v]) low[u]=std::min(low[u],dfn[v]);
	}
	if(low[u]==dfn[u]){
		++scccnt;
		do{
			scc[stack[--top]]=scccnt;
		}while(stack[top]^u);
	}
}
int main(){
	n=read();m=read();
	for(reg int u,v,uw,vw,i=1;i<=m;i++){
		u=read();uw=read();v=read();vw=read();
		if(uw&&vw){
			G.add(u+n,v);G.add(v+n,u);
		}
		else if(!uw&&!vw){
			G.add(u,v+n);G.add(v,u+n);
		}
		else{
			if(uw) std::swap(u,v);
			G.add(u,v);G.add(v+n,u+n);
		}
	}
	for(reg int i=1;i<=n*2;i++)if(!dfn[i]) tarjan(i);
	for(reg int i=1;i<=n;i++)if(scc[i]==scc[i+n]) return std::puts("IMPOSSIBLE"),0;
	std::puts("POSSIBLE");
	for(reg int i=1;i<=n;i++) std::printf("%d ",scc[i]<scc[i+n]);
	return 0;
}