2-CNF-SAT Problem

原理

若要滿足 2-CNF-SAT 代表每個子句都必須為 True，而每個子句的格式為

$(A\vee B)$。又

$(A\vee B)$ 等價於

$(\mathrm{\neg }A\Rightarrow B)$ 和

$(\mathrm{\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); 
}