「学习笔记」2-SAT

一.什么是 \(\text{2-SAT}\)

\(SAT\) 是适定性 \(Satisfiability\) 问题的简称。一般形式为 \(k -\)适定性问题，简称 \(\text{k-SAT}\)。而当 \(k>2\) 时，该问题为 \(NP\) 完全的。所以我们只研究 \(k=2\) 的情况。

形象地来说，给定 \(n\) 个布尔变量 \(a_i\)，同时给出若干个约束条件：

\((\text{not})a_i\) \(op\) \((\text{not})a_j = \text{true/false}\)。

而求解 \(\text{2-SAT}\) 就是求出一组 \(a_i\) 的解。

二.将 \(\text{2-SAT}\) 问题转换为图论问题

首先定义一条有向边的定义 \(x\to y\)：如果满足 \(x\) 就必须满足 \(y\)。

发现一个点有两个状态真或假，可以想到将点 \(u\) 拆为点 \(u_0,u_1\)，分别表示假或真。

\(1.\) \(a\land b = \text{true}\) \(\to (a1, b1),(b1, a1)\)。

\(2.\) \(a\land b = \text{false}\) \(\to (a1, b0),(b1, a0)\)。

\(3.\) \(a\lor b = \text{true}\) \(\to (a0, b1),(b0, a1)\)。

\(4.\) \(a\lor b = \text{false}\) \(\to (a0, b0),(b0, a0)\)。

这样我们就将 \(\text{2-SAT}\) 问题转换为图论问题了，可以运用图论的方式解决。

三.解决 \(\text{2-SAT}\) 问题

• \(1.\) 判断有无解

  由上文定义的状态可以得知，\(u_0\) 和 \(u_1\) 不能同时被满足。
  那么存在点 \(x_0\) 和 \(x_1\) 在同一个强连通分量中时，那么无解。
  反之则有解。

• \(2.\) 求方案

  由我们的建边可得：对于每个点 \(u\)，选择其拓扑序较大的那种状态更优。
  为什么呢？
  如下图所示：
  

  对于 \(x1\) 的两种状态，如果选择 \(\text{false}\)，那么推导出 \(x2\) 为 \(\text{true}\)，又推导出 \(x1\) 为 \(\text{true}\)，又推导出 \(x2\) 为 \(\text{false}\)，发现这种解法矛盾了。
  但如果对于 \(x1\) 选择 \(\text{true}\)，那么 \(x2\) 为 \(\text{false}\)，则满足要求。
  由此我们得出：对于每个点 \(u\)，选择其拓扑序较大的那种状态更优。
  这里不需要再做一遍拓扑排序求拓扑序，在 \(\text{Tarjan}\) 求强连通分量中就求出了每个点的逆拓扑序，每个点的强连通分量编号也就是逆拓扑序。

四.例题讲解

标签：false,text,拓扑,笔记,学习,b0,true,SAT
来源： https://www.cnblogs.com/chenyuhe/p/15872977.html