2-CNF-SAT Problem
===
### 原理
若要滿足 2-CNF-SAT 代表每個子句都必須為 True，而每個子句的格式為 $(A \vee B)$。又 $(A \vee B)$ 等價於 $(\neg A \Rightarrow B)$ 和 $(\neg B \Rightarrow A)$。意義上為「如果 A(B) 為假，則 B(A) 一定要是真」，如此才能滿足 $(A \vee B)$ 為真。

解法是將 Boolean formula 建構成一個 Implication Graph 來找解，建構方式請參考如下演算法。現在先來討論哪種情況不滿足 2-SAT，
* Case 1 : 存在邊 $(X_i, \hat X_i)$，代表如果 $X_i$ 為真，則 $\hat X_i$ 也要為真，推得 $X_i$ 為假，產生矛盾。故此種情況不可能 Satisfiable。
* Case 2 : 存在邊 $(\hat X_i, X_i)$，代表如果 $\hat X_i$ 為真，則 $X_i$ 也要為真，但前提已假設 $X_i$ 為假，產生矛盾。故此種情況不可能 Satisfiable。
* Case 3 : $X_i$ 和 $\hat X_i$ 在同一個強連通分量中。代表存在一條 Implication Path 可以從 $X_i$ 走回 $\hat X_i$，令該路徑為 $X_i \Rightarrow X_{j} \Rightarrow X_{k} \Rightarrow ... \Rightarrow \hat X_i$。如果 $X_i$ 設為 True，則中間經過的每個布林變數也要設為 True，最後設 $\hat X_i$ 為 True，推得 $X_i$ 為 False，產生矛盾。故此種情況不可能 Satisfiable。
### 演算法
假設 Boolean formula 有 n 種布林變數，m 個子句
1. 將 Boolean formula 轉成一有向圖 G (Implication Graph) :
建構方式 :
(1) 對每個 $x_i$，新增兩個點 $X_i$ 和 $\hat X_i$
(2) 對每個子句 $(x_i \vee x_j)$，新增兩條有向邊 $(\hat X_i, X_j)$ 和 $(\hat X_j, X_i)$
2. 利用 Kosaraju's Algorithm 找出所有強連通分量。
3. 檢查每組 $x_i$ 和 $\hat x_i$ 是否在同一個強連通分量中。如果存在一組相同代表 Unsatisfiable 則回傳 False。若每組 $x_i$ 和 $\hat x_i$ 都在不同的強連通分量中，代表此 Boolean formula 為 Satisfiable，回傳 True。
### 時間 : O(n + m)
Step 1 : O(n + m)
Step 2 : O(V + E) = O(2n + 2m) = O(n + m)
Step 3 : O(n)

故 2-CNF-SAT 可在多項式時間內解決。
### 實作

#include <bits/stdc++.h> 
using namespace std; 
const int MAX = 100000; 

vector<int> adj[MAX]; 
vector<int> adjInv[MAX]; // Inverse Graph 
bool visited[MAX]; 
bool visitedInv[MAX]; // Inverse Graph
stack<int> s; // DFS 用
int scc[MAX]; // 紀錄每個點屬於哪個 SCC 
int counter = 1; // SCC 數量 
 
void addEdges(int a, int b) { 
    adj[a].push_back(b); 
} 

void addEdgesInverse(int a, int b) { 
    adjInv[b].push_back(a); 
} 

void dfsFirst(int u) { 
    if(visited[u]) return; 
    visited[u] = 1; 
    for (int i = 0; i < adj[u].size(); i++) 
    	dfsFirst(adj[u][i]);
    s.push(u); 
} 

void dfsSecond(int u) { 
    if(visitedInv[u]) return; 
    visitedInv[u] = 1; 
    for (int i = 0; i < adjInv[u].size(); i++) 
    	dfsSecond(adjInv[u][i]); 

    scc[u] = counter; // 將此點編號在第 cnt 個 SCC
} 

void is2Satisfiable(int n, int m, int a[], int b[]) { 
    for(int i = 0; i < m; i++) {
        // 變數 x (正數)對應到點 x
        // x 補數 (-x) 對應到點 n + x，因為對應計算方式為 n-(-x)
	// 如果變數 x 本身為負數的話，它的補數就直接加負號就可以了 => -x
        // 對每個子句 a[i] or b[i]，新增邊 -a[i] -> b[i] 和 -b[i] -> a[i] 
	if (a[i] > 0 && b[i] > 0) { 
	    addEdges(a[i] + n, b[i]); 
	    addEdgesInverse(a[i] + n, b[i]); 
	    addEdges(b[i] + n, a[i]); 
	    addEdgesInverse(b[i] + n, a[i]); 
	} 
	else if (a[i] > 0 && b[i] < 0) { 
	    addEdges(a[i] + n, n - b[i]); 
	    addEdgesInverse(a[i] + n, n - b[i]); 
	    addEdges(-b[i], a[i]); 
	    addEdgesInverse(-b[i], a[i]); 
	} 
	else if (a[i] < 0 && b[i] > 0) { 
	    addEdges(-a[i], b[i]); 
	    addEdgesInverse(-a[i], b[i]); 
	    addEdges(b[i] + n, n - a[i]); 
	    addEdgesInverse(b[i] + n, n - a[i]); 
	} 
	else{ 
	    addEdges(-a[i], n - b[i]); 
	    addEdgesInverse(-a[i], n - b[i]); 
	    addEdges(-b[i], n - a[i]); 
	    addEdgesInverse(-b[i], n - a[i]); 
	} 
    } 
	
    // Kosaraju's Algorithm 第一步
    for (int i = 1; i <= 2 * n ; i++) 
	if (!visited[i]) dfsFirst(i); 
  
    // Kosaraju's Algorithm 第二步拜訪 Inverse Graph
    while (!s.empty()) { 
	int n = s.top(); 
	s.pop(); 

	if (!visitedInv[n]) { 
	    dfsSecond(n); 
	    counter++; 
	} 
    } 

    for (int i = 1; i <= n; i++) {
        // 若存在變數 x 和 -x 待在同一個 SCC 則不可能 SAT
	if(scc[i]==scc[i+n]) { 
            cout << "The given expression is unsatisfiable." << endl; 
	    return; 
	} 
    } 
    
    // 每個變數 x 和 -x 都不在相同 SCC 中則滿足 SAT
    cout << "The given expression is satisfiable." << endl; 
} 

int main() { 
    // n 為布林變數種類，m 為子句數量
    int n = 5, m = 7;  

    // 每個子句的形式為 (a or b)，且有 m 個子句
    // 所以建立兩個大小為 m 的陣列 a 和 b 來存放 Boolean Formula 的輸入
    // 例如用 a[i] or b[i] 來表示第 i 個子句
    // 對每個變數 x，其範圍 1 <= x <= N，而 x 的補數為
    // -N <= -x <= -1   
    int a[] = {1, -2, -1, 3, -3, -4, -3}; 
    int b[] = {2, 3, -2, 4, 5, -5, 4}; 
    // (x1+x2)*(x2’+x3)*(x1’+x2’)*(x3+x4)*(x3’+x5)*(x4’+x5’)*(x3’+x4)

    is2Satisfiable(n, m, a, b); 
}