A.2-sat簡介

2-sat算法可以求解給定推出關系下的一種合法情況。題目中重常常，給定一些布爾變量A、B、C、D…，再給出一系列形如$B?A,C??D$的推出關系，詢問使得所有推出關系都成立的一組布爾變量取值。

B.2-sat算法內容

1.無解情況

一個變量要么為真，要么為假，不能同時為真又為假。
如果 $A??A$，那該變量不能取值為真，因為，為真就觸發矛盾
如果 $?A?A$，那該變量不能取值為假，因為，為假就觸發矛盾
所以，如果 $A??A$，$?A?A$，就找不到合法解。
其余情況有解。

2.構造合法解

嘗試貪心地構造一組合法解。
觀察這樣一組情況
$A??B?C??A?D?B$
由于關系的傳遞性，

• 如果A為真，后面5個變量都要合法，即 B為假，C為真，A為假，D為真，B為真。不難發現，A為真且為假，B為真且為假，矛盾。
• 如果A為假，只需最后3個變量合法，即D為真，B為真。

得出結論，對于變量A，選擇拓撲序靠后一個，更優。具體一些，嚴格優于另一個。
推廣到一般，對于任意變量X，選擇拓撲序靠后的取值為答案中的值。

3.算法實現

1. 首先，需要建圖。假設共有n個變量，點 1,2,3…n表示變量為真情況，點 1 + n，2 + n，…n+n表示變量為假的情況。對于第 i 個變量，點 i 表示該變量為真， 點 i + n表示該變量為假。往每個點中存入由該點能推出的點，例如，

• 變量 n 為真 推出 變量 1 為真，則往點n中存入1；
• 變量 n 為真 推出 變量 1 為假，則往點n中存入 1 + n；
• 變量 n 為假 推出 變量 1 為假，則往點n + n中存入 1

2. 判斷無解情況，對整個圖求強聯通分量，如果 i 與 i + n在一個強聯通分量內部，則存在上文所說的 “$A??A$，$?A?A$”，則無解。
3. 如果有解，對每個變量，輸出拓撲序靠后的一個，即強聯通分量編號小的一個（tarjan算法的性質）。

\\tarjan
const int N = 1e6 + 10;
int dfn[N],low[N],cnt;
stack<int> stk;
bool ins[N];
int id[N],scc_cnt,sz[N];
vector<int> g[N];
int n,m;void tarjan(int u)
{dfn[u] = low[u] = cnt ++;stk.push(u);ins[u] = 1;for(auto j : g[u]){if(!dfn[j]){tarjan(j);low[u] = min(low[u],low[j]);}else if(ins[j]){low[u] = min(low[u],dfn[j]);}}if(dfn[u] == low[u]){int y;++scc_cnt;do{y = stk.top();stk.pop();ins[y] = 0;id[y] = scc_cnt;sz[scc_cnt] ++;}while(y != u);}
}

	\\判斷有無解for(int i = 1; i <= 2*n; i ++){if(!dfn[i]) tarjan(i);}for(int i = 1; i <= n; i ++){if(id[i] == id[i+n]){cout << "NO\n";return;}}

	\\存儲答案vector<int> ans;for(int i = 1; i <= n; i ++){if(id[i] < id[i + n])ans.push_back(i);}

例題 P4782 【模板】2-SAT

題目描述

有 $n$ 個布爾變量 $x_1～x_n$，另有 $m$ 個需要滿足的條件，每個條件的形式都是 「$x_i$ 為 true / false 或 $x_j$ 為 true / false」。比如 「$x_1$ 為真或 $x_3$ 為假」、「$x_7$ 為假或 $x_2$ 為假」。

2-SAT 問題的目標是給每個變量賦值使得所有條件得到滿足。

輸入格式

第一行兩個整數 $n$ 和 $m$，意義如題面所述。

接下來 $m$ 行每行 $4$ 個整數 $i$, $a$, $j$, $b$，表示 「$x_i$ 為 $a$ 或 $x_j$ 為 $b$」( a , b ∈ { 0 , 1 } a, b\in \{0,1\} a,b∈{0,1})

輸出格式

如無解，輸出 IMPOSSIBLE；否則輸出 POSSIBLE。

下一行 $n$ 個整數 $x_1～x_n$（ x i ∈ { 0 , 1 } x_i\in\{0,1\} xi?∈{0,1}），表示構造出的解。

輸入輸出樣例 #1

輸入 #1

3 1
1 1 3 0

輸出 #1

POSSIBLE
0 0 0

說明/提示

$1\le n,m\le 10^6$ , 前 $3$ 個點卡小錯誤，后面 $5$ 個點卡效率。

由于數據隨機生成，可能會含有（ 10 0 10 0）之類的坑，但按照最常規寫法的寫的標程沒有出錯，各個數據點卡什么的提示在標程里。

思路

• $A\vee B??A?B,?B?A$

練習

【2018ICPC首爾區域賽】
【2023ICPC濟南區域賽】
【2023ICPC網絡預選賽(2)】