2-CNF-SAT Problem

原理

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

(AB)。又
(AB)
等價於
(¬AB)
(¬BA)
。意義上為「如果 A(B) 為假,則 B(A) 一定要是真」,如此才能滿足
(AB)
為真。

解法是將 Boolean formula 建構成一個 Implication Graph 來找解,建構方式請參考如下演算法。現在先來討論哪種情況不滿足 2-SAT,

  • Case 1 : 存在邊
    (Xi,X^i)
    ,代表如果
    Xi
    為真,則
    X^i
    也要為真,推得
    Xi
    為假,產生矛盾。故此種情況不可能 Satisfiable。
  • Case 2 : 存在邊
    (X^i,Xi)
    ,代表如果
    X^i
    為真,則
    Xi
    也要為真,但前提已假設
    Xi
    為假,產生矛盾。故此種情況不可能 Satisfiable。
  • Case 3 :
    Xi
    X^i
    在同一個強連通分量中。代表存在一條 Implication Path 可以從
    Xi
    走回
    X^i
    ,令該路徑為
    XiXjXk...X^i
    。如果
    Xi
    設為 True,則中間經過的每個布林變數也要設為 True,最後設
    X^i
    為 True,推得
    Xi
    為 False,產生矛盾。故此種情況不可能 Satisfiable。

演算法

假設 Boolean formula 有 n 種布林變數,m 個子句

  1. 將 Boolean formula 轉成一有向圖 G (Implication Graph) :
    建構方式 :
    (1) 對每個
    xi
    ,新增兩個點
    Xi
    X^i

    (2) 對每個子句
    (xixj)
    ,新增兩條有向邊
    (X^i,Xj)
    (X^j,Xi)
  2. 利用 Kosaraju's Algorithm 找出所有強連通分量。
  3. 檢查每組
    xi
    x^i
    是否在同一個強連通分量中。如果存在一組相同代表 Unsatisfiable 則回傳 False。若每組
    xi
    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); }