标签：解决 关系 题解 字典 有一个 过程 组合 缩点 运算
设 $n$ 个布尔变量 $f_1, f_2, ..., f_n$ .
给定 $m$ 个形如 " 变量 - 逻辑运算符 - 变量 " 的二元限制条件, 例如 $f_1 ~ and ~ f_2$ .
解布尔变量.
就现在的研究层次, 我们要解决的问题是 存在性 层次的相关问题:
① 解什么时候存在.
② 构造一组合法解.
③ 构造一组字典序最小的解.
我们将每个布尔变量 $f_x$ , 拆成两个点 $x, x‘$ , $x$ 代表 true , $x‘$ 代表 false .
我们定义蕴含关系:
如果选择了点 $x$ , 那么必须选择点 $y$ .
对应地, 我们在图中连边 $x \rightarrow y$ .
蕴含关系具有传递性.
举个例子: $f_x ~ or ~ f_y$ 应该如何连边?
若 $f_x$ 为假, 则 $f_y$ 必然为真. ---- ①
逆否命题: 若 $f_y$ 为假, 则 $f_x$ 必然为真. ---- ②
我们发现 ①② 不仅是必要条件, 同时也是充分条件, 即 $f_x ~ or ~ f_y \Leftrightarrow ①②$ .
所以我们连边 $x‘ \rightarrow y, y‘ \rightarrow x$ .
我们不难发现, 建出来的图是左右对称的.
那么, 我们现在的问题被转化为:
① 在图中的每个点对中选择一个点.
② 若一个点被选择, 则它的所有后继都要被选择.
我们考虑对这张图跑 Tarjan 算法, 求强连通分量.
并对所有的强连通分量, 按照结束访问的时间, 从小到大进行标号.
如果存在 $x, x‘$ 在同一个强连通分量内, 那么一定无解.
因为选择了 $x$ 就必须要选择 $x‘$ , 选择了 $x‘$ 就 $x$ , 而我们目标每个点对中选择一个.
否则, 我们可以尝试构造性地证明一定有解.
我们如果选择了某个强连通分量内的点, 那么整个强连通分量都要选择.
我们按照强连通分量, 将图进行缩点.
现在的问题和原问题的形式是一致的:
① 现在的点是原本的强连通分量.
② 我们有 $m$ 个点对.
③ 每个点 $x$ 具有一个标号 $L_x$ .
④ 图具有左右对称的性质.
⑤ 我们要在每个点对中选择一个点, 且如果一个点被选择, 那么它的所有后继都要被选择.
点的标号存在一些性质.
如果存在边 $x \rightarrow y$ , 那么 $L_y < L_x$ .
证明
① 当我们访问 $x$ 的时候, 还没有访问到 $y$ , 那么一定会先结束访问 $y$ .
② 当我们访问 $x$ 的时候, 已经访问过 $y$ , 那么 $y$ 在 $x$ 前先结束访问.
我们对于每个点对 $(x, y)$ , 选择标号小的点.
证明:
① 我们对每个点对 $(x, y)$ , 选择标号小的点, 那么已经能满足 "每个点对中选择一个点" 的约束条件.
② 证明 "如果一个点被选择, 那么它的所有后继都要被选择." .
假设原图中存在点 $x$ , 它有后继 $y$ , 我们选择了点 $x$ , 却没有选择点 $y$ .
那么有
$$\begin{aligned} L_y & > L_{y‘} & (选择了 y‘ 却没有选择 y) \\ & > L_{x‘} & (图的对称性 + 标号性质) \\ & > L_x & (选择了 x 却没有选择 x‘) \\ & > L_y & (标号性质) \end{aligned}$$
所以矛盾, 所以必然不存在这种情况.
总结一些, 我们得到了两个重要的结论:
① 2-SAT 问题有解, 当且仅当不存在 $x$, $x‘$ , $x$ 和 $x‘$ 在同一个强连通分量内.
② 若 2-SAT 问题有解, 那么我们对每对强连通分量, 取标号较小的, 即对每个变量 $f_x$ , 取它对应的强连通分量的标号较小的.
有些问题中还增加了一元限制条件 $not ~ f_x$ , $f_x$ .
$not ~ f_x \Rightarrow (x \rightarrow x‘)$ .
$f_x \Rightarrow (x‘ \rightarrow x)$ .
我们尝试兼容这种情况, 即尝试对构造性证明加以补充.
若 $x \rightarrow x‘$ , 那么必然选择 $x‘$ .
而对于标号必有 $L_{x‘} < L_x$ , 根据构造性证明的过程, 必然选择 $L_{x‘}$ .
二者得以统一.
标签：解决 关系 题解 字典 有一个 过程 组合 缩点 运算
原文地址：http://www.cnblogs.com/Sdchr/p/7389219.html
