主要内容
(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)」。对于每条二元限制，将其对应的命题与逆否命题的边连上，缺一不可。
-
对于 $a_i = operatorname{true} $ 连边 $ eg a_i ightarrow a_i $ 「可以理解为：表示如果 (i) 选了
false那么 (i) 必须要是true与 (i) 只能选一个true或者false矛盾，强迫 (i) 只能是true」。 -
对于 $a_i = operatorname{false} $ 连边 $ a_i ightarrow eg a_i $
-
对于 $ a operatorname{or} b = operatorname{true}$，连边 $ eg a ightarrow b $ 和 $ eg b ightarrow a$ 「可以理解为：若 (a) 假则 (b) 必真，若 (b) 假则 (a) 必真」。
-
对于 $ a operatorname{or} b = operatorname{false}$，连边 $a ightarrow eg a $ 和 $ b ightarrow eg b$
-
对于 $ a operatorname{and} b = operatorname{false}$，连边 $a ightarrow eg b $ 和 $ b ightarrow eg a$
-
对于 $ a operatorname{and} b = operatorname{true}$，连边 $ eg a ightarrow a $ 和 $ eg b ightarrow b$
-
对于 $ a e b $，连边 $a ightarrow eg b $ 、 $ eg a ightarrow b $ 、 $b ightarrow eg a $ 、 $ eg b ightarrow a $
-
对于 $ 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}) 的时间复杂度 。
核心代码：
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;