『筆記』2-SAT
阿新 • • 發佈：2021-03-08
# **前置**
> $SAT$ 是適定性（ $Satisfiability$ ）問題的簡稱。一般形式為 $k \ -$ 適定性問題，簡稱 $k-SAT$ 。而當 $k>2$ 時該問題為 $NP$ 完全的。所以我們只研究 $k=2$ 的情況。
# **定義**
> $2-SAT$ ，簡單的說就是給出 $n$ 個集合，每個集合有兩個元素，已知若干個 $$ ，表示 $a$ 與 $b$ 矛盾（其中 $a$ 與 $b$ 屬於不同的集合）。然後從每個集合選擇一個元素，判斷能否一共選 $n$ 個兩兩不矛盾的元素。顯然可能有多種選擇方案，一般題中只需要求出一種即可。
有學長者雲：
> 有 $n$ 個 $01$ 變數 $x_1∼x_n$，另有 $m$ 個變數取值需要滿足的限制。
>
> 每個限制是一個 $$ 元組 $(x_{p1},x_{p2},\dots,x_{pk})$ ，滿足 $x_{p1} \oplus x_{p2} \oplus \dots \oplus x_{pk} = a$ 。其中 $a$ 是 $0/1$ ，$\oplus$ 是某種二元 $bool$ 運算。
>
> 要求構造一種滿足所有限制的變數的賦值方案。
$2-SAT$ 問題是通過**建立圖論模型**，在 $O(n+m)$ 的時間複雜度內判斷是否有解，若有解可以構造出一組合法解。
# **思路**
值得注意的是在不同的題目中二元 $bool$ 運算可能有差異，但是建圖的基本思路大致相同。
來觀摩一組 ```OI-Wiki``` 的例子：
> 比如邀請人來吃喜酒，夫妻二人必須去一個，然而某些人之間有矛盾（比如 $A$ 先生與 $B$ 女士有矛盾， $C$ 女士不想和 $D$ 先生在一起），那麼我們要確定能否避免來人之間沒有矛盾，有時需要方案。這是一類生活中常見的問題。
>
> 使用布林方程表示上述問題。設 $a$ 表示 $A$ 先生去參加，那麼 $B$ 女士就不能參加（ $\lnot a$）； $b$ 表示 C 女士參加，那麼 $\lnot b$ 也一定成立（ $D$ 先生不參加）。總結一下，即 $(a \lor b)$ （變數 $a$ ， $b$ 至少滿足一個）。對這些變數關係建有向圖，則有：$\lnot a \Rightarrow b \land \lnot b \Rightarrow a$ （ $a$ 不成立則 $b$ 一定成立；同理，$b$ 不成立則 $a$ 一定成立）。建圖之後，我們就可以使用**縮點**演算法來求解 $2-SAT$ 問題了。
# **核心**
## **Tarjan 縮點大法**
> $Tarjan$ 大法好！
主要還是考慮如何更合適地**建圖**。
再來一組例子：
假設有 $a_1$ 、 $b_2$ 和 $a_2$ 、 $b_1$ 兩對，已知 $a_1$ 和 $b_2$ 間有矛盾，於是為了方案自洽，由於兩者中必須選一個，所以我們就要拉兩條有向邊 $(a_1,b_1)$ 和 $(b_2,a_2)$ 表示選了 $a_1$ 則必須選 $b_1$ ，選了 $b_2$ 則必須選 $a_2$ 才能夠自洽。
然後通過這樣建邊再跑一遍 $Tarjan$ 判斷是否有一個集合中的兩個元素在同一個**強連通分量**中，若有則不可能，否則輸出方案。構造方案只需要把幾個不矛盾的強連通分量拼起來就好了。
+ 輸出方案時可以通過變數在圖中的拓撲序確定該變數的取值。如果變數 $\lnot x$ 的拓撲序在 $x$ 之後，那麼取 $x$ 值為真。應用到 $Tarjan$ 演算法的縮點，即 $x$ 所在強連通分量編號在 $\lnot x$ 之前時，取 $x$ 為真。因為 $Tarjan$ 演算法求強連通分量時使用了棧，所以 $Tarjan$ 求得的強連通分量編號相當於反拓撲序。
+ 時間複雜度為 $O(n+m)$ 。
## **暴力DFS**
> ~~$Tarjan$ 好？ $DFS$ 表示不服。~~
>
> $DFS$ 大法妙！
直接選取圖上一個點，沿著一條路徑搜下去，如果一個點被選擇了，那麼這條路徑以後的點都將被選擇。
如果出現**一個集合中的兩者**都被選擇了，那麼此即為矛盾情況。
# **例題**
[P4782 【模板】2-SAT 問題](https://www.luogu.com.cn/problem/P4782)
> 真·模板題
## **思路**
+ 這是一道模板題。
+ 顯而易見每個變數 $x_i$ 都可以被分開儲存，即拆分成 $i$ 和 $i+n$ ，分別表示 $x_i=1$ 和 $x_i=0$ ，則這兩個事件是互斥的。
+ 對於限制 $x_i$ 的每個命題 $a$ 和 $b$ ，一定有一個為真，則可以寫成
$$
\lnot a \Rightarrow b \\
\lnot b \Rightarrow a
$$
那麼由此可連邊建圖 $(\lnot a,b)$ ， $(\lnot b,a)$ 。
+ 在該圖中，若節點 $i$ 與 $i+n$ 在同一個強連通分量中，即允許互相到達，則它們分別代表的互斥事件會同時發生，說明存在矛盾，即不存在一組合法的方案。
+ 否則則有解。
+ 構造合法解：
+ 對原圖縮點得到一張 $DAG$ 。
+ > 對於變數 $x_i$，考察節點 $i$ 與 $i+n$ 所在強連通分量的拓撲關係。若兩分量不連通，則 $xi$ 可取任意一個值。否則只能取屬於拓撲序較大的分量的值。因為若取拓撲序較小的值，可以根據邏輯關係推出取另一個值也是同時發生的。
>
> by @LuckyBlock
+ $Tarjan$ 演算法賦給強連通分量的編號順序與拓撲序是相反的，上文已有說明。
## **CODE**
```cpp
/*
Name: P4782 【模板】2-SAT 問題
By Frather_
*/
#include
#include
#include
#include
#include
using namespace std;
/*=========================================快讀*/
int read()
{
int x = 0, f = 1;
char c = getchar();
while (c < '0' || c > '9')
{
if (c == '-')
f = -1;
c = getchar();
}
while (c >= '0' && c <= '9')
{
x = (x << 3) + (x << 1) + (c ^ 48);
c = getchar();
}
return x * f;
}
/*=====================================定義變數*/
int n, m;
const int _ = 5000050;
struct edge
{
int to;
int nxt;
} e[_];
int cnt, head[_];
int dfn[_], low[_], num;
int bel[_], b_num;
stack s;
/*===================================自定義函式*/
void add(int from, int to)
{
e[++cnt].to = to;
e[cnt].nxt = head[from];
head[from] = cnt;
}
void Tarjan(int u_)
{
dfn[u_] = low[u_] = ++num;
s.push(u_);
for (int i = head[u_]; i; i = e[i].nxt)
{
int v_ = e[i].to;
if (!dfn[v_])
{
Tarjan(v_);
low[u_] = min(low[u_], low[v_]);
}
else if (!bel[v_])
low[u_] = min(low[u_], dfn[v_]);
}
if (dfn[u_] == low[u_])
{
b_num++;
while (true)
{
int t = s.top();
s.pop();
bel[t] = b_num;
if (t == u_)
break;
}
}
return;
}
/*=======================================主函式*/
int main()
{
n = read();
m = read();
for (int i = 1; i <= m; i++)
{
int x = read();
int a = read();
int y = read();
int b = read();
if (a && b)
{
add(x + n, y);
add(y + n, x);
}
if (!a && b)
{
add(x, y);
add(y + n, x + n);
}
if (!a && !b)
{
add(x, y + n);
add(y, x + n);
}
if (a && !b)
{
add(x + n, y + n);
add(y, x);
}
}
for (int i = 1; i <= n * 2; i++)
{
if (!dfn[i])
Tarjan(i);
if (i <= n && bel[i] == bel[i + n])
{
printf("IMPOSSIBLE\n");
return 0;
}
}
printf("POSSIBLE\n");
for (int i = 1; i <= n; i++)
printf("%d ", bel[i] < bel[i + n]);
return 0;
}
```
# **寫在最後**
+ 最近被教練抓頹抓得好苦啊\kk
+ 再次向已逝去的學長致敬（（（不是
+ 鳴謝：
+ 《演算法競賽進階指南》
+ [OI-Wiki](oi-wiki.org)
+ @Lu