演算法學習筆記：2-SAT
阿新 • • 發佈：2020-08-07
> SAT 是適定性（Satisfiability）問題的簡稱。一般形式為 k - 適定性問題，簡稱 k-SAT。而當 $k>2$ 時該問題為 NP 完全的。所以我們只研究 $k=2$ 的情況。
## 定義
2-SAT，簡單的說就是給出 $n$ 個集合，每個集合有兩個元素，已知若干個 $$ ，表示 $a$ 與 $b$ 矛盾（其中 $a$ 與 $b$ 屬於不同的集合）。然後從每個集合選擇一個元素，判斷能否一共選 $n$ 個兩兩不矛盾的元素。顯然可能有多種選擇方案，一般題中只需要求出一種即可。
## 現實意義
比如邀請人來吃喜酒，夫妻二人必須去一個，然而某些人之間有矛盾（比如 A 先生與 B 女士有矛盾，C 女士不想和 D 先生在一起），那麼我們要確定能否避免來人之間沒有矛盾，有時需要方案。這是一類生活中常見的問題。
使用布林方程表示上述問題。設 $a$ 表示 A 先生去參加，那麼 B 女士就不能參加（ $\neg a$ )； $b$ 表示 C 女士參加，那麼 $\neg b$ 也一定成立（D 先生不參加）。總結一下，即 $(a \vee b)$ （變數 $a, b$ 至少滿足一個）。對這些變數關係建有向圖，則有： $\neg a\Rightarrow b\wedge\neg b\Rightarrow a$ （ $a$ 不成立則 $b$ 一定成立；同理， $b$ 不成立則 $a$ 一定成立）。建圖之後，我們就可以使用縮點演算法來求解 2-SAT 問題了。
## 常用解決方法
### Tarjan [SCC 縮點](https://www.cnblogs.com/RioTian/p/13444771.html)
演算法考究在建圖這點，我們舉個例子來講：
假設有 ${a1,a2}$ 和 ${b1,b2}$ 兩對，已知 $a1$ 和 $b2$ 間有矛盾，於是為了方案自洽，由於兩者中必須選一個，所以我們就要拉兩條條有向邊 $(a1,b1)$ 和 $(b2,a2)$ 表示選了 $a1$ 則必須選 $b1$ ，選了 $b2$ 則必須選 $a2$ 才能夠自洽。
然後通過這樣子建邊我們跑一遍 Tarjan SCC 判斷是否有一個集合中的兩個元素在同一個 SCC 中，若有則輸出不可能，否則輸出方案。構造方案只需要把幾個不矛盾的 SCC 拼起來就好了。
輸出方案時可以通過變數在圖中的拓撲序確定該變數的取值。如果變數 $\neg x$ 的拓撲序在 $x$ 之後，那麼取 $x$ 值為真。應用到 Tarjan 演算法的縮點，即 $x$ 所在 SCC 編號在 $\neg x$ 之前時，取 $x$ 為真。因為 Tarjan 演算法求強連通分量時使用了棧，所以 Tarjan 求得的 SCC 編號相當於反拓撲序。
顯然地，時間複雜度為 $O(n+m)$ 。
### 爆搜
就是沿著圖上一條路徑，如果一個點被選擇了，那麼這條路徑以後的點都將被選擇，那麼，出現不可行的情況就是，存在一個集合中兩者都被選擇了。
那麼，我們只需要列舉一下就可以了，資料不大，答案總是可以出來的。
#### 爆搜模板
下方程式碼來自劉汝佳的白書：
```cpp
// 來源：白書第 323 頁
struct Twosat {
int n;
vector g[maxn * 2];
bool mark[maxn * 2];
int s[maxn * 2], c;
bool dfs(int x) {
if (mark[x ^ 1]) return false;
if (mark[x]) return true;
mark[x] = true;
s[c++] = x;
for (int i = 0; i < (int)g[x].size(); i++)
if (!dfs(g[x][i])) return false;
return true;
}
void init(int n) {
this->n = n;
for (int i = 0; i < n * 2; i++) g[i].clear();
memset(mark, 0, sizeof(mark));
}
void add_clause(int x, int y) { // 這個函式隨題意變化
g[x].push_back(y ^ 1); // 選了 x 就必須選 y^1
g[y].push_back(x ^ 1);
}
bool solve() {
for (int i = 0; i < n * 2; i += 2)
if (!mark[i] && !mark[i + 1]) {
c = 0;
if (!dfs(i)) {
while (c > 0) mark[s[--c]] = false;
if (!dfs(i + 1)) return false;
}
}
return true;
}
};
```
## 例題
### **HDU3062 [Party](http://acm.hdu.edu.cn/showproblem.php?pid=3062) **
> 題面：有 n 對夫妻被邀請參加一個聚會，因為場地的問題，每對夫妻中只有 $1$ 人可以列席。在 $2n$ 個人中，某些人之間有著很大的矛盾（當然夫妻之間是沒有矛盾的），有矛盾的 $2$ 個人是不會同時出現在聚會上的。有沒有可能會有 $n$ 個人同時列席？
這是一道多校題，裸的 2-SAT 判斷是否有方案，按照我們上面的分析，如果 $a1$ 中的丈夫和 $a2$ 中的妻子不合，我們就把 $a1$ 中的丈夫和 $a2$ 中的丈夫連邊，把 $a2$ 中的妻子和 $a1$ 中的妻子連邊，然後縮點染色判斷即可。
```cpp
#include