2-SAT 总结
albertting
·
·
算法·理论
近期学习了 2-SAT，于是来总结一下！！
:::warning[观前提示]{open}
建议先了解2-SAT 是什么和基本求解方式。
:::
UPD：感谢__NikaidoHiro__指出，sinz 的第三条子句 y_{i-1} 全部写少了一个 \neg，抱歉喵。
简要的基本知识
2-SAT 可以规约成图论问题，图上有向边即为命题的推出关系。可以使用 Tarjan 或 Kosaraju 等算法求 scc 并判断一个命题和其否命题是否在同一 scc 内，若在则等价，不合法。对于一个命题和它的否命题，可以通过定 DAG 上拓扑序靠后的命题为真来构造一组解，因为若一个命题为真 DAG 上它的后继都为真，为了保证解的合法性取一定不会发生冲突的靠后命题。
建图规则
建图的基本顺序是：
- 把约束写成若干“必须为真的子句”；
- 每个子句连边。
一些基本逻辑的推导
折叠框包裹，可以先思考（？）
按照推导顺序，从易到难。
1. 蕴含 a\Rightarrow b（“a 真则 b 真”）
::::success[答案]
连边：
a\to b,\neg b\to\neg a
:::warning[为什么有两条？]
:::
::::
#### 2. NAND（$\neg a\vee\neg b$，“$a$ 和 $b$ 不能同真”）
::::success[答案]
连边：
$$
a\to\neg b,b\to\neg a
$$
“一个真另一个必须为假”的直观理解。
这两个命题恰好互为逆否命题。
::::
#### 3. 析取（$a\vee b$，逻辑或）
::::success[答案]
连边：
$$
\neg a\to b,\neg b\to a
$$
其实就是反的 NAND，只不过 NAND 更直观一些。
::::
#### 4. 等价 $a\Leftrightarrow b
::::success[答案]
连边：
a\to b,b\to a,\neg a\to\neg b,\neg b\to\neg a
5. 异或 a\oplus b
::::success[答案]
连边：
a\to\neg b,b\to\neg a,\neg a\to b,\neg b\to a
NAND 加强版，不仅要两个不同真，也要两个不同假。
异或可以写作：
(a\vee b)\wedge(\neg a\vee\neg b)
6. 否定约束 a=\neg b
::::success[答案]
连边：
a\to\neg b,b\to\neg a,\neg a\to b,\neg b\to a
:::warning[你这不是和异或一样吗]
对的其实我没有写错，这两个东西就是等价的喵。可以简单推一下。
:::
::::
7. 单位子句（强制取值）
::::success[答案]
关键结论：a 等价于 a\vee a。于是可以按照析取来做！
若强制为真连边：
\neg a\to a
:::warning[什么你说为啥反向不用连边]
恭喜！你和我犯了一样的错误。
| 首先肯定反向连边就变成 a\Leftrightarrow\neg a 直接不合法了，其次你仔细观察一下析取的式子就会发现推出来两条边是一样的（） |
若强制为否连边：
a\to\neg a
8. 合取（a\wedge b，逻辑与）
::::success[答案]
连边：
\neg a\to a,\neg b\to b
有了以上知识，你就可以游刃有余解决 2-SAT 的基本建模了！
例题：https://codeforces.com/gym/104120/problem/E
2-SAT 全家桶！注意数据范围！
建图基础技巧
中转点
若有两个集合 S_1 和 S_2，对于所有 S_1 中的命题全部需要连向 S_2 中连边，可以加入中转点 p 传递推出的关系，具体做法是 S_1 中所有点连向 p，p 连向 S_2 中所有点。
链式约束
实际上就是省去一些冗余连边，白嫖命题推出关系的传递性，想的时候就应该考虑了，可能不算什么技巧。
拆拆拆大子句
析取大子句
(x_1\vee\cdots\vee x_k)\Rightarrow y\equiv\bigwedge_{i=1}^k\neg(x_i\wedge\neg y)=\bigwedge_{i=1}^k(\neg x_i\vee y)
常见公式，关键在于 (x_1\vee\cdots\vee x_k)\Rightarrow y\equiv\neg(x_1\vee\cdots\vee x_k)\vee y。中间一步的式子是容易直观理解的。
:::warning[y\Rightarrow(x_1\vee\cdots\vee x_k) 为何不行]
这个东西是 (k+1)-SAT，无法拆成二元子句。
:::
合取大子句
y\Rightarrow(x_1\wedge\cdots\wedge x_k)\equiv\bigwedge_{i=1}^k\neg(y\wedge\neg x_i)=\bigwedge_{i=1}^k(\neg y\vee x_i)
同样的，中间一句是容易理解的。
:::warning[不说反过来的是因为它是 k+1-SAT 吗]
对。
:::
sinz 编码
显然可以连 $\binom{k}{2}$ 个 NAND，但是这个太爆炸了是 $O(k^2)$ 的。
可以引入辅助变量 $y_i$ 表示 $x_1\dots x_i$ 中已经有真的，连三个子句组：
$$
\neg x_i\vee y_i,\neg y_{i-1}\vee y_i,\neg x_i\vee\neg y_{i-1}
$$
分别含义为：若 $x_i$ 为真前缀一定存在真的，$y$ 单调传递（一旦变为真后继必须均为真），$x_i$ 为真和前面已为真不能同时。
如果把这三个写作合取为假的形式：
$$
\neg(x_i\wedge\neg y_i),\neg(y_{i-1}\wedge\neg y_i),\neg(x_i\wedge y_{i-1})
$$
是容易理解的。
### 区间连边
即 $x\to y_j$，$j\in[l,r]$，并且存在多个 $x$ 和多组区间时，可以在 $y$ 上建立线段树，非 leaf 的节点作为区间辅助节点。这是中转点的推广技巧。若有单组约束产生 $O(\log k)$ （$k$ 为区间长度）。
或者两侧均为区间，可以简单做到 $O(\log^2 k)$，但是可以结合中转点做到 $O(\log k)$，即左侧非 leaf 点连向中转点再连向右侧非 leaf 点。