2-SAT

2-SAT 问题

和网络流一样，很多问题都可以建模为 2-SAT 问题，只要会求解 2-SAT，就可以解决许多问题。

洛谷博客
github
vercel

k-SAT

首先引入 k-SAT 问题。

k-SAT 问题说的就是有 $n$ 个布尔值 $a_i$ 和 $m$ 组约束条件，其中每组约束都是 $a$ 中 $k$ 个值进行逻辑运算后等于一个给定值 （$0$ 或 $1$） 的形式，求一组满足约束的 $a_i$（或者输出无解）。

比如

$\begin{cases} (a_0 \operatorname{and} a_1) \operatorname{or} (\operatorname{not} a_2)\operatorname{and} a_3=1\\ (a_0 \operatorname{xor} (\operatorname{not}a_1)) \operatorname{and} a_2 =0\\ (a_0 \operatorname{or} a_1) \operatorname{xor} (\operatorname{not} a_2)=1 \end{cases}$

是一个 3-SAT 问题，它的一个解为

$\begin{cases} a_0=0\\ a_1=0\\ a_2=0\\ a_3=1 \end{cases}$

可以证明 k-SAT 在 $k\ge3$ 时是没有多项式解法的，但是 $k\le2$ 时有。

2-SAT

2-SAT 问题是 k-SAT 问题在 $k=2$ 时的特例。

每一个约束条件都可以表示为 「$a_i$ 为 $x$ 或 $a_j$ 为 $y$」的形式。和网络流一样，很多问题都可以建模为 2-SAT 问题，只要会求解 2-SAT，就可以解决许多问题。建模当然比原算法难哈哈哈

接下来是重点：如何求解 2-SAT 问题。

1. 图论建膜

先建立膜型 stO CYB Orz

我们把每个变量拆成两个点，一个表示该变量为真，另一个表示该变量为假。我们约定 $\left<i,x\right>$ 为 $a_i=x$ 代表的节点，如 $\left<10,1\right>$ 表示 $a_{10}=1$ 代表的节点。因此一个节点代表了一个命题。既然这样，我们就可以自然地定义节点 $\left<i,x\right>$ 的非节点 $\neg\left<i,x\right>$ 定义为 $\left<i,\neg x\right>$，表示 $a_i\not= x$ 也就是 $a_i=\neg x$。

边表示蕴含关系，即 $\left<i,x\right>$ 到 $\left<j,y\right>$ 间有一条有向边表示如果 $a_i=x$ 则 $a_j=y$。注意连边时要把这条边的逆否边连起来，$\left<i,x\right> \to \left<j,y\right>$ 则 $\left<j,\neg y\right> \to \left<i,\neg x\right>$。为了方便，我们把 $\left<i,x\right>$ 能走到 $\left<j,y\right>$ 记为 $\left<i,x\right> \Rightarrow \left<j,y\right>$，走不到记为 $\left<i,x\right> \not\Rightarrow \left<j,y\right>$。

则原问题可化为：在约束对应的图上，选择 $n$ 个点，使表示某变量为真与为假的点有且只有一个被选择，每个点若被选择，它能走到的节点也被选择。

2. 求解

怎么解呢？当然要请出我们的 爆搜 Tarjan 大佬。

首先我们发现，如果一个节点与它的非节点互相连通，那么问题肯定无解，因为如果 $a_i=1\Rightarrow a_i=0$ 且 $a_i=0\Rightarrow a_i=1$，那么就形成了逻辑矛盾。

然后我们发现，如果 $\left<i,x\right> \Rightarrow \left<i,\neg x\right>$ 且 $\left<i,\neg x\right> \not\Rightarrow \left<i,x\right>$ 则 $a_i=\neg x$。（其实也就是反证法）

如果 $\left<i,x\right>$ 与 $\left<i,\neg x\right>$ 没有直接或间接关系，则 $a_i$ 可以随便取值。

因此我们考虑将图用 tarjan 把强连通分量缩点，得到一张 DAG。如果一个点和它的非节点在同一个强连通分量中，则问题无解，否则，$a_i$ 的取值就是 $\left<i,1\right>$ 和 $\left<i,0\right>$ 中缩点后拓扑序较小的节点，因为拓扑序较大的节点不可能走回拓扑序小的节点。

于是，我们得到了一组可行解。

code

// by juruo999
#include<iostream>
#include<cstdio>
#include<cstring>
#include<algorithm>
#include<vector>

using namespace std;

namespace sat{

	const int maxn=1000006;
	vector<int> e[maxn*2];

	int n;
	inline int rho(int i,bool x){	// <i,x>
		return i*2-x;
	}
	void add(int i,bool a,int j,bool b){	// x[i]==a => x[j]==b
		e[rho(i,a)].push_back(rho(j,b));
		e[rho(j,b^1)].push_back(rho(i,a^1));
	}

	int dfn[maxn*2],low[maxn*2],vis[maxn*2],cnt=0;
	int scc[maxn*2],sccn=0,stk[maxn*2],tp=0;
	void dfs(int u){
		low[u]=dfn[u]=++cnt;
		stk[++tp]=u;
		vis[u]=1;
		for(int i=e[u].size()-1;i>=0;i--){
			int v=e[u][i];
			if(!dfn[v]){
				dfs(v);
				low[u]=min(low[u],low[v]);
			}else if(vis[v]){
				low[u]=min(low[u],dfn[v]);
			}
		}
		if(low[u]==dfn[u]){
			sccn++;
			while(stk[tp]!=u){
				vis[stk[tp]]=0;
				scc[stk[tp]]=sccn;
				tp--;
			}
			vis[stk[tp]]=0;
			scc[stk[tp]]=sccn;
			tp--;
		}
	}
	
	bool x[maxn];
	bool solve(){
		for(int i=1;i<=2*n;i++){
			if(!dfn[i]){ dfs(i); }
		}
		for(int i=1;i<=n;i++){
			if(scc[rho(i,0)]==scc[rho(i,1)]){
				return 0;
			}else{
				x[i]=scc[rho(i,0)]>scc[rho(i,1)];
			}
		}
		return 1;
	}

	bool& get(int i){
		return x[i];
	}

}

using sat::e;
using sat::rho;

int n,m;

int main(){

	scanf("%d%d",&n,&m);
	
	sat::n=n;
	for(int i=1;i<=m;i++){
		int x,a,y,b;
		scanf("%d%d%d%d",&x,&a,&y,&b);
		sat::add(x,a^1,y,b);
	}

	if(sat::solve()){
		puts("POSSIBLE");
		for(int i=1;i<=n;i++){
			printf("%d%c",sat::x[i]," \n"[i==n]);
		}
	}else{
		puts("IMPOSSIBLE");
	}

	return 0;

}

例题

模板题
双倍经验
NOI2017 游戏

第三题有一些难度，我做这道题的时候一开始建模建错了，结果不能保证每个地图都能分配到赛车……