SAT 问题，即要求对一些 bool 变量赋值满足一定关系。对于 $k$-SAT 问题（$k \geq 3$），学术界已经证明是 NP-Complete 的。因此，只研究 2-SAT 问题。

2-SAT 问题有一些约束条件，每个条件形如 $x_i$ 为 （ 真 / 假 ） （ 与 / 或 ） $x_j$ 为 （ 真 / 假 ）。

考虑这些约束条件都意味着什么。以 $x$ 为真 或 $y$ 为假做例子。

若 $x$ 为假，则要想成立，$y$ 必为假。

若 $y$ 为真，则要想成立，$x$ 必为真。

即：$\neg x \rightarrow \neg y,y \rightarrow x$。

既然这样，不如，建模成图？

给每个 $x$ 和 $\neg x$ 都分配节点，然后连边。

连好之后，你会发现，所有同一个强连通分量里的点，要么全部成立，要么全部不成立。

所以，若 $x$ 和 $\neg x$ 在一个强连通分量里，则无解。

若有解，我们就在 $x$ 和 $\neg x$ 中取拓扑序较大的成立。证明见 解析。