2-SAT

主要内容

(operatorname{2~-~SAT})，简单的说就是给出 (n) 个集合，每个集合有两个元素，已知若干个 (<a,b>) ，表示 (a) 与 (b) 矛盾（其中 (a) 与 (b) 属于不同的集合）。然后从每个集合选择一个元素，判断能否一共选 (n) 个两两不矛盾的元素。显然可能有多种选择方案，一般题中只需要求出一种即可 。

解决方法

使用强连通分量。

存图

对于每个变量 (x)，我们建立两个点：(x, eg x) 分别表示变量 (x) 取 true 和取 false。所以， 图的节点个数是两倍的变量个数 。在存储方式上，可以给第 (i) 个变量标号为 (i)，其对应的反值标号为 (i + n)。

建图

边 (u ightarrow v) 表示 「若 (u) 则 (v)」，其逆否命题为 ( eg v ightarrow eg u)，表示「若非 (v) 则非 (u)」。对于每条二元限制，将其对应的命题与逆否命题的边连上，缺一不可。

1. 对于 $a_i = operatorname{true} $ 连边 $ eg a_i ightarrow a_i $ 「可以理解为：表示如果 (i) 选了 false 那么 (i) 必须要是 true 与 (i) 只能选一个 true 或者 false 矛盾，强迫 (i) 只能是 true」。

2. 对于 $a_i = operatorname{false} $ 连边 $ a_i ightarrow eg a_i $

3. 对于 $ a operatorname{or} b = operatorname{true}$，连边 $ eg a ightarrow b $ 和 $ eg b ightarrow a$ 「可以理解为：若 (a) 假则 (b) 必真，若 (b) 假则 (a) 必真」。

4. 对于 $ a operatorname{or} b = operatorname{false}$，连边 $a ightarrow eg a $ 和 $ b ightarrow eg b$

5. 对于 $ a operatorname{and} b = operatorname{false}$，连边 $a ightarrow eg b $ 和 $ b ightarrow eg a$

6. 对于 $ a operatorname{and} b = operatorname{true}$，连边 $ eg a ightarrow a $ 和 $ eg b ightarrow b$

7. 对于 $ a e b $，连边 $a ightarrow eg b $ 、 $ eg a ightarrow b $ 、 $b ightarrow eg a $ 、 $ eg b ightarrow a $

8. 对于 $ a = b $，连边 $ a ightarrow b $ 、 $ eg a ightarrow eg b $ 、 $b ightarrow a $ 、 $ eg b ightarrow eg a $

可以看到，同一强连通分量内的变量值一定是相等的。也就是说，如果 (x) 与 ( eg x) 在同一强连通分量内部，一定无解。反之，就一定有解了。

但是，对于一组布尔方程，可能会有多组解同时成立。判断给每个布尔变量赋的值，只需要 当 (x) 所在的强连通分量的拓扑序在 ( eg x) 所在的强连通分量的拓扑序之后取 (x) 为真就可以了。

注：在使用 (operatorname{Tarjan}) 算法缩点找强连通分量的过程中，已经为每组强连通分量标记好顺序了——不过是反着的拓扑序。所以一定要写成 color[x] > color[-x] 。

时间复杂度：(O(n + m)) ，即 (operatorname{Tarjan}) 的时间复杂度 。

• P4782 【模板】2-SAT 问题

• P4171 [JSOI2010]满汉全席

核心代码：

void tarjan(int u)
{
	 dfn[u]=low[u]=++Time; s.push(u),ins[u]=true;
	 for(int i=hea[u];i;i=nex[i])
	 {
	 	 if(!dfn[ver[i]]) tarjan(ver[i]),low[u]=min(low[u],low[ver[i]]);
	 	 else if(ins[ver[i]]) low[u]=min(low[u],dfn[ver[i]]);
	 }
	 if(dfn[u]==low[u])
	 {
	 	 sum++;
	 	 do u=s.top(),s.pop(),ins[u]=false,belong[u]=sum;
		 while(dfn[u]!=low[u]);
	 }
}

for(int i=1;i<=n*2;i++) if(!dfn[i]) tarjan(i);
for(int i=1;i<=n;i++) if(belong[i*2-1]==belong[i*2]) exist=false;