可满足性问题（Satisfiability, SAT），又称适定性问题，是算法中的一类经典问题。

概述

2-SAT

设有 n 个二元组 (a_1, b_1), \dots, (a_n, b_n)，希望从每个二元组中都选取一个元素，但是同时要求一些元素不能同时选择，例如 a_1 和 b_1 不能同时选择、a_2 和 a_3 不能同时选择……问是否存在一种可行的选择，使得所有的条件都能得到满足。这一问题称为 2-SAT 问题。

k-SAT

设 x_1, \dots, x_n 是 n 个布尔变量，给定形如

的合取范式，其中每个子句 c_i 都由 k 个变量（x_j）或其取反（\neg x_j）的逻辑或得到：

其中 a_l 为 x_j 或者 \neg x_j。k-SAT 问题就是：是否存在 x_1, \dots, x_n 的某种取值，使得 F(x_1, \dots, x_n) 为真。

对于 k \ge 3，k-SAT 问题已经被证明是 NP 完全问题。因此在算法竞赛中通常只考虑 2-SAT 问题。

2-SAT 与强连通分量

转化

2-SAT 的每个条件都可以分解为一些条件命题的并。例如 a_1 和 b_2 不能同时出现，就等价于当 a_1 出现时，必定不选 b_2（即必定选择 a_2），且 b_2 出现时，必定不选 a_1（即必定选择 b_1）。由此，我们可以将 2-SAT 问题转化为一些形如 a_i \to a_j 的条件命题的合取。

如果我们将选择 a_i 表示为 x_i = 1，将选择 b_i 表示为 x_i = 0，那么 a_1 和 b_2 不能同时出现，也就是必须选择 b_1 或者选择 a_2，即 \neg x_1 \lor x_2。这一析取式可以等价写为

从而一个析取式可以转化为两个条件式的合取。

建立有向图，初始时有 2n 个节点，每个节点对应取 a_i 或者取 b_i。对于条件 u \to v，在有向图上添加一条有向边 u \to v。由于条件命题的传递性，有向图上节点 u 可达节点 v，就表示选了 u 的同时就必定要选 v。

如果对于一个二元组 (a_i, b_i)，有 a_i 可达 b_i 且 b_i 可达 a_i，则说明条件存在矛盾，命题不可满足。这一条件等价于 a_i, b_i 位于有向图的同一个强连通分量之中，因此，只需要求出强连通分量后，逐一判断所有二元组是否属于同一连通分量即可。

一般使用 （链接未公开） 的 Tarjan 算法来解决这一问题。对 2-SAT 问题建图的时间复杂度是 O(n + m)，求 SCC 的时间复杂度是 O(n + m)，判断的复杂度是 O(n)，故最终复杂度是 O(n + m)。

可以验证，对 3-SAT 问题，每个句子并不一定能转化为条件命题，因此这种方法只对 2-SAT 有效。

优化建边

使用强连通分量解决 2-SAT 问题，对于条件命题 u \to v，未必需要建立有向边 u \to v，而是只要保证 u 可达 v 即可。当条件特别多但是有规律时，就可以利用各种方法优化建边。

Targan 算法的时间复杂度是 O(|V| + |E|)，优化建边可以减少 |E| 的大小，优化时间复杂度。

例题：ICPC 2023 网络赛第二场 C. Covering

题意：给定一个数组 (a_1, \dots, a_n)（n \le 2 \times 10^5），从 1, \dots, n 选取若干下标 i_1 < i_2 < \dots < i_k < n，满足以下条件：

• 对任意 i_j \ne i_k，有 a_{i_j} \ne a_{i_k} 或者 a_{i_j + 1} \ne a_{i_k + 1}；
• 对任意 x = 1, \dots, n，存在下标 i_k 满足 i_k = x 或 i_k + 1 = x。