【模板】2-SAT 问题

【模板】2-SAT 问题

通用做法：拆点+Tarjan求强连通分量。将点(i)拆为(i)和(i+n)，分别表示(i)为假以及(i)为真。注意这个顺序不能搞反，否则求可行解的时候会出错。

连边：

本题中给出的命题为：“(x)为(a)或(y)为(b)”。以“(x)为真或(y)为假”为例，连边时作以下考虑：

• 若(x)为假，则(y)必须为假，命题才能成立，故连边(x→y)

• 若(y)为真，则(x)必须为真，命题才能成立，故连边(y+n→x+n)

连边完成。

显然当(i)与(i+n)在同一个强连通分量中时，无论怎样取值都无法满足全部命题，此时无解。

当输出布尔变量(i)的可行解时，只需输出强连通分量编号较小的那一个取值即可，即：

for(int i=1;i<=n;i++){
	if(sccno[i+n]<sccno[i]) cout<<"1 ";
	else cout<<"0 ";
}