若要滿足 2-CNF-SAT 代表每個子句都必須為 True,而每個子句的格式為
解法是將 Boolean formula 建構成一個 Implication Graph 來找解,建構方式請參考如下演算法。現在先來討論哪種情況不滿足 2-SAT,
假設 Boolean formula 有 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);
}