2-SAT
SAT 是适定性（Satisfiability）问题的简称．一般形式为 k - 适定性问题，简称 k-SAT．而当 𝑘 >2k>2
时该问题为 NP 完全的．所以我们只研究 𝑘 =2k=2 的情况．
定义
2-SAT，简单的说就是给出 𝑛n 个布尔方程，每个方程和两个变量相关，如 𝑎 ∨𝑏a∨b，表示变量 𝑎,𝑏a,b 至少满足一个．然后判断是否存在可行方案，显然可能有多种选择方案，一般题中只需要求出一种即可．另外，¬𝑎¬a 表示 𝑎a 取反．
解决思路
有 𝑛n 个布尔变量 𝑥1 ∼𝑥𝑛x1∼xn，另有 𝑚m 个需要满足的条件，每个条件的形式都是「𝑥𝑖xi 为 true/false 或 𝑥𝑗xj 为 true/false」．比如「𝑥1x1 为真或 𝑥3x3 为假」、「𝑥7x7 为假或 𝑥2x2 为假」．
2-SAT 问题的目标是给每个变量赋值使得所有条件得到满足．
使用布尔方程表示上述问题．设 𝑎a 表示 𝑥𝑎xa 为真（¬𝑎¬a 就表示 𝑥𝑎xa 为假）．如果有个人提出的要求分别是 𝑎a 和 𝑏b，即 (𝑎 ∨𝑏)(a∨b)（变量 𝑎,𝑏a,b 至少满足一个）．对这些变量关系建有向图，则把 𝑎a 成立或不成立用图中的点表示，¬𝑎 →𝑏¬a→b ¬𝑏 →𝑎¬b→a，表示 𝑎a 不成立 则 𝑏b 一定成立 ；同理，𝑏b 不成立 则 𝑎a 一定成立 ．建图之后，我们就可以使用缩点算法来求解 2-SAT 问题了．
| 原式 | 建图 |
|---|---|
| ¬𝑎 ∨𝑏¬a∨b | 𝑎 →𝑏a→b 和 ¬𝑏 →¬𝑎¬b→¬a |
| 𝑎 ∨𝑏a∨b | ¬𝑎 →𝑏¬a→b 和 ¬𝑏 →𝑎¬b→a |
| ¬𝑎 ∨¬𝑏¬a∨¬b | 𝑎 →¬𝑏a→¬b 和 𝑏 →¬𝑎b→¬a |
许多 2-SAT 问题都需要找出如 𝑎a 不成立 ，则 𝑏b 成立 的关系．
求解
思考如果两点在同一强连通分量里有什么含义．根据前文边的逻辑意义可知：若两点在同一强连通分量内，则这两点代表的条件 要么都满足，要么都不满足 ．
建图后我们使用 Tarjan 算法找 SCC，判断对于任意布尔变量 𝑎a，表示 𝑎a 成立的点和表示 𝑎a 不成立的点是否在同一个 SCC 中（同一条件不可能既满足又不满足，或既不满足又并非不满足），若有则输出无解，否则有解．
输出方案时可以通过变量在图中的拓扑序确定该变量的取值．如果变量 𝑥x 的拓扑序在 ¬𝑥¬x 之后，那么取 𝑥x 值为真．应用到 Tarjan 算法的缩点，即 𝑥x 所在 SCC 编号在 ¬𝑥¬x 之前时，取 𝑥x 为真．因为 Tarjan 算法求强连通分量时使用了栈，如果跑完 Tarjan 缩点之后呈现出的拓扑序更大，在 Tarjan 会更晚被遍历到，就会更早地被弹出栈而缩点，分量编号会更小，所以 Tarjan 求得的 SCC 编号相当于 反拓扑序 ．
算法会把整张图遍历一遍，由于这张图 𝑛n 和 𝑚m 同阶，计算答案时复杂度为 𝑂(𝑛)O(n)，因此总复杂度为 𝑂(𝑛)O(n)．
代码实现
---|---
## 例题
### 例题 1
[HDU3062 Party](https://acm.hdu.edu.cn/showproblem.php?pid=3062)
有 𝑛n 对夫妻被邀请参加一个聚会，因为场地的问题，每对夫妻中只有一人可以列席．在 2𝑛2n 个人中，某些人之间有着很大的矛盾（当然夫妻之间是没有矛盾的），有矛盾的两个人是不会同时出现在聚会上的．有没有可能会有 𝑛n 个人同时列席？
按照上面的分析，如果 𝑎1a1 中的丈夫和 𝑎2a2 中的妻子不合，我们就把 𝑎1a1 中的丈夫和 𝑎2a2 中的丈夫连边，把 𝑎2a2 中的妻子和 𝑎1a1 中的妻子连边，然后缩点染色判断即可．
参考代码
---|---
例题 2
2018-2019 ACM-ICPC Asia Seoul Regional K TV Show Game
有 𝑘k 盏灯，每盏灯是红色或者蓝色，但是初始的时候不知道灯的颜色．有 𝑛n 个人，每个人选择三盏灯并猜灯的颜色．一个人猜对两盏灯或以上的颜色就可以获得奖品．判断是否存在一个灯的着色方案使得每个人都能领奖，若有则输出一种灯的着色方案．
根据 伍昱 -《由对称性解 2-sat 问题》，我们可以得出：如果要输出 2-SAT 问题的一个可行解，只需要在 tarjan 缩点后所得的 DAG 上自底向上地进行选择和删除．
具体实现的时候，可以通过构造 DAG 的反图后在反图上进行拓扑排序实现；也可以根据 tarjan 缩点后，所属连通块编号越小，节点越靠近叶子节点这一性质，优先对所属连通块编号小的节点进行选择．
下面给出第二种实现方法的代码．
参考代码
---|---
## 习题
* [洛谷 P5782 和平委员会](https://www.luogu.com.cn/problem/P5782)
* [POJ3683 Priest John's Busiest Day](http://poj.org/problem?id=3683)
* * *
> __本页面最近更新： 2026/1/7 08:56:54，[更新历史](https://github.com/OI-wiki/OI-wiki/commits/master/docs/graph/2-sat.md)
> __发现错误？想一起完善？[在 GitHub 上编辑此页！](https://oi-wiki.org/edit-landing/?ref=/graph/2-sat.md "edit.link.title")
> __本页面贡献者：[AndrewWayne](https://github.com/AndrewWayne), [Ir1d](https://github.com/Ir1d), [Tiphereth-A](https://github.com/Tiphereth-A), [Backl1ght](https://github.com/Backl1ght), [chu-yuehan](https://github.com/chu-yuehan), [Early0v0](https://github.com/Early0v0), [Enter-tainer](https://github.com/Enter-tainer), [frank-xjh](https://github.com/frank-xjh), [H-J-Granger](https://github.com/H-J-Granger), [akakw1](https://github.com/akakw1), [algosheep](https://github.com/algosheep), [Anguei](https://github.com/Anguei), [c-forrest](https://github.com/c-forrest), [felixesintot](https://github.com/felixesintot), [guodong2005](https://github.com/guodong2005), [HeRaNO](https://github.com/HeRaNO), [jpy-cpp](https://github.com/jpy-cpp), [kenlig](https://github.com/kenlig), [Konano](https://github.com/Konano), [ksyx](https://github.com/ksyx), [ouuan](https://github.com/ouuan), [sshwy](https://github.com/sshwy)
> __本页面的全部内容在**[CC BY-SA 4.0](https://creativecommons.org/licenses/by-sa/4.0/deed.zh) 和 [SATA](https://github.com/zTrix/sata-license)** 协议之条款下提供，附加条款亦可能应用