1. 2-SAT
1.1. 介绍
对于一些节点，每个节点存在两个状态（非 \(0\) 即 \(1\)），我们给出一些如下类型的限制条件：
- 节点 \(i\) 状态为 \(1/0\)。
- 若节点 \(i\) 状态为 \(1/0\)，那么节点 \(j\) 状态为 \(1/0\)。
- 节点 \(i,j\ (i\not=j)\) 至少有一个为 \(1/0\)。
2-SAT 算法用于解决类似的问题，每个节点最多只能有两种状态。
我们用有向图表示节点状态之间的递推关系，我们设 \(p_i\) 表示节点 \(i\) 状态为真，我们将上述限制条件写为表达式并写为“若 \(p\) ，则 \(q\)”的形式，便于用有向图表示它们的关系：
- \(p_i\)：若 \(\lnot p_i\)，则 \(p_i\)。
- \(\lnot p_i\)：若 \(p_i\)，则 \(\lnot p_i\)。
- \(p_i\lor p_j\)：若 \(\lnot p_i\) 则 \(p_j\)；若 \(\lnot p_j\) 则 \(p_i\)。
- \(\lnot p_i\lor\lnot p_j\)：若 \(p_i\) 则 \(\lnot p_j\)；若 \(p_j\) 则 \(\lnot p_i\)。
- \(\lnot p_i\lor p_j\)：若 \(p_i\) 则 \(p_j\)；若 \(\lnot p_j\) 则 \(\lnot p_i\)。
若有 \(p\Rightarrow q\)，并且 \(p,q\) 相互矛盾，则 \(p\) 一定为假。
更进一步地，若有 \(p\Leftrightarrow q\)，并且 \(p,q\) 相互矛盾，则此限制条件下，无解。
考虑无解的情况在有向图中的表现形式，即两个矛盾状态在图中处于同一个强连通分量中，我们考虑用 Tarjan 算法进行缩点。
对于一种可行方案则在 \(p_i,\lnot p_i\) 两个状态点中选择拓扑序更小的即可，用 Tarjan 后可省去拓扑排序过程，详见我其他博客。
1.2. 例题
咕咕咕