\(SAT\) 是适定性（ \(Satisfiability\) ）问题的简称。一般形式为 \(k \ -\) 适定性问题，简称 \(k-SAT\) 。而当 \(k>2\) 时该问题为 \(NP\) 完全的。所以我们只研究 \(k=2\) 的情况。
定义\(2-SAT\) ，简单的说就是给出 \(n\) 个集合，每个集合有两个元素，已知若干个 \(<a,b>\) ，表示 \(a\) 与 \(b\) 矛盾（其中 \(a\) 与 \(b\) 属于不同的集合）。然后从每个集合选择一个元素，判断能否一共选 \(n\) 个两两不矛盾的元素。显然可能有多种选择方案，一般题中只需要求出一种即可。
有学长者云：
有 \(n\) 个 \(01\) 变量 \(x_1∼x_n\)，另有 \(m\) 个变量取值需要满足的限制。
每个限制是一个 $$ 元组 \((x_{p1},x_{p2},\dots,x_{pk})\) ，满足 \(x_{p1} \oplus x_{p2} \oplus \dots \oplus x_{pk} = a\) 。其中 \(a\) 是 \(0/1\) ，\(\oplus\) 是某种二元 \(bool\) 运算。
要求构造一种满足所有限制的变量的赋值方案。
\(2-SAT\) 问题是通过建立图论模型，在 \(O(n+m)\) 的时间复杂度内判断是否有解，若有解可以构造出一组合法解。
思路值得注意的是在不同的题目中二元 \(bool\) 运算可能有差异，但是建图的基本思路大致相同。
来观摩一组 OI-Wiki 的例子：
比如邀请人来吃喜酒，夫妻二人必须去一个，然而某些人之间有矛盾（比如 \(A\) 先生与 \(B\) 女士有矛盾， \(C\) 女士不想和 \(D\) 先生在一起），那么我们要确定能否避免来人之间没有矛盾，有时需要方案。这是一类生活中常见的问题。
使用布尔方程表示上述问题。设 \(a\) 表示 \(A\) 先生去参加，那么 \(B\) 女士就不能参加（ \(\lnot a\)）； \(b\) 表示 C 女士参加，那么 \(\lnot b\) 也一定成立（ \(D\) 先生不参加）。总结一下，即 \((a \lor b)\) （变量 \(a\) ， \(b\) 至少满足一个）。对这些变量关系建有向图，则有：\(\lnot a \Rightarrow b \land \lnot b \Rightarrow a\) （ \(a\) 不成立则 \(b\) 一定成立；同理，\(b\) 不成立则 \(a\) 一定成立）。建图之后，我们就可以使用缩点算法来求解 \(2-SAT\) 问题了。
核心 Tarjan 缩点大法\(Tarjan\) 大法好！
主要还是考虑如何更合适地建图。
再来一组例子：
假设有 \(a_1\) 、 \(b_2\) 和 \(a_2\) 、 \(b_1\) 两对，已知 \(a_1\) 和 \(b_2\) 间有矛盾，于是为了方案自洽，由于两者中必须选一个，所以我们就要拉两条有向边 \((a_1,b_1)\) 和 \((b_2,a_2)\) 表示选了 \(a_1\) 则必须选 \(b_1\) ，选了 \(b_2\) 则必须选 \(a_2\) 才能够自洽。
然后通过这样建边再跑一遍 \(Tarjan\) 判断是否有一个集合中的两个元素在同一个强连通分量中，若有则不可能，否则输出方案。构造方案只需要把几个不矛盾的强连通分量拼起来就好了。
输出方案时可以通过变量在图中的拓扑序确定该变量的取值。如果变量 \(\lnot x\) 的拓扑序在 \(x\) 之后，那么取 \(x\) 值为真。应用到 \(Tarjan\) 算法的缩点，即 \(x\) 所在强连通分量编号在 \(\lnot x\) 之前时，取 \(x\) 为真。因为 \(Tarjan\) 算法求强连通分量时使用了栈，所以 \(Tarjan\) 求得的强连通分量编号相当于反拓扑序。
时间复杂度为 \(O(n+m)\) 。
暴力DFS\(Tarjan\) 好？ \(DFS\) 表示不服。
\(DFS\) 大法妙！
直接选取图上一个点，沿着一条路径搜下去，如果一个点被选择了，那么这条路径以后的点都将被选择。
如果出现一个集合中的两者都被选择了，那么此即为矛盾情况。
例题P4782 【模板】2-SAT 问题
真·模板题
思路
这是一道模板题。
显而易见每个变量 \(x_i\) 都可以被分开存储，即拆分成 \(i\) 和 \(i+n\) ，分别表示 \(x_i=1\) 和 \(x_i=0\) ，则这两个事件是互斥的。
对于限制 \(x_i\) 的每个命题 \(a\) 和 \(b\) ，一定有一个为真，则可以写成
\[\lnot a \Rightarrow b \\ \lnot b \Rightarrow a \]