摘自oiwiki

假设有 {a1,a2} 和 {b1,b2} 两对，已知 a1 和 b2 间有矛盾，于是为了方案自洽，由于两者中必须选一个，所以我们就要拉两条有向边 (a1,b1) 和 (b2,a2) 表示选了 a1 则必须选 b1，选了 b2 则必须选 a2 才能够自洽。 然后通过这样子建边我们跑一遍 Tarjan SCC 判断是否有一个集合中的两个元素在同一个 SCC 中，若有则输出不可能，否则输出方案。构造方案只需要把几个不矛盾的 SCC 拼起来就好了。 输出方案时可以通过变量在图中的拓扑序确定该变量的取值。如果变量 x 的拓扑序在 $\neg$ x 之后，那么取 x 值为真。应用到 Tarjan 算法的缩点，即 x 所在 SCC 编号在 $\neg$ x 之前时，取 x 为真。因为 Tarjan 算法求强连通分量时使用了栈，所以 Tarjan 求得的 SCC 编号相当于反拓扑序。

所以说为什么：如果变量 x 的拓扑序在 $\neg$ x 之后，那么取 x 值为真