ปัญหา 2-Satisfiability (2-SAT) ใน C/C++

ภาพรวม

2-SAT (2-Satisfiability) เป็นกรณีพิเศษของ SAT Problem ที่แต่ละ Clause มีตัวแปร 2 ตัว: (x₁ ∨ y₁) ∧ (x₂ ∨ y₂) ∧ ... ∧ (xₙ ∨ yₙ)

แตกต่างจาก General SAT (NP-Complete) 2-SAT แก้ได้ใน Polynomial Time (O(n+m))

การลดรูปเป็น Graph Problem

แปลงแต่ละ Clause (x ∨ y) เป็น 2 Implications:

• ¬x → y
• ¬y → x

สร้าง Implication Graph ที่มี 2n โหนด (ตัวแปร n ตัว + การปฏิเสธ n ตัว)

เงื่อนไข Satisfiable

Formula เป็น Satisfiable ก็ต่อเมื่อ สำหรับทุกตัวแปร xᵢ: xᵢ และ ¬xᵢ ไม่อยู่ใน SCC เดียวกัน

อัลกอริทึม (Kosaraju's SCC)

1. สร้าง Implication Graph (2n vertices, 2m edges)
2. หา Strongly Connected Components (SCCs) ด้วย Kosaraju หรือ Tarjan
3. ตรวจสอบ: ถ้ามี i ที่ comp[xᵢ] == comp[¬xᵢ] → UNSAT
4. ถ้า SAT: กำหนดค่าตัวแปรตาม Topological Order ของ SCCs
   • ถ้า comp[¬xᵢ] > comp[xᵢ] (¬xᵢ อยู่หลังใน Topo Order) → xᵢ = TRUE
   • Else → xᵢ = FALSE

Pseudocode (Kosaraju)

// First DFS - Fill Stack by Finish Time
dfs1(v):
    visited[v] = true
    for u in adj[v]:
        if not visited[u]: dfs1(u)
    stack.push(v)

// Second DFS on Transposed Graph - Assign Components
dfs2(v, label):
    comp[v] = label
    for u in adjT[v]:
        if comp[u] == -1: dfs2(u, label)

// Main
for i = 1 to n:
    addEdge(¬xᵢ, yᵢ)
    addEdge(¬yᵢ, xᵢ)

for each vertex v:
    if not visited[v]: dfs1(v)

reverse all edges (or use adjT)

label = 0
while stack not empty:
    v = stack.pop()
    if comp[v] == -1:
        dfs2(v, label++)
        
for i = 1 to n:
    if comp[xᵢ] == comp[¬xᵢ]: return UNSAT
    
// Assignment
for i = 1 to n:
    xᵢ = (comp[xᵢ] > comp[¬xᵢ])  // Higher topo order = True

โค้ดตัวอย่าง C++ (โครงสร้างหลัก)

#include <bits/stdc++.h>
using namespace std;

class TwoSAT {
    int n;  // Variables count
    vector<vector<int>> adj, adjT;
    vector<int> comp, order, assignment;
    vector<bool> visited;

    int var(int x) { return x > 0 ? 2*(x-1) : 2*(-x-1); }      // x -> 2*(x-1)
    int neg(int x) { return x > 0 ? 2*(x-1)+1 : 2*(-x-1); }    // ¬x -> opposite

public:
    TwoSAT(int n) : n(n), adj(2*n), adjT(2*n), comp(2*n, -1), visited(2*n), assignment(n) {}

    void addClause(int x, int y) {  // (x ∨ y)
        int nx = neg(x), ny = neg(y);
        adj[nx].push_back(var(y));
        adj[ny].push_back(var(x));
        adjT[var(y)].push_back(nx);
        adjT[var(x)].push_back(ny);
    }

    void dfs1(int v) {
        visited[v] = true;
        for (int u : adj[v]) if (!visited[u]) dfs1(u);
        order.push_back(v);
    }

    void dfs2(int v, int cl) {
        comp[v] = cl;
        for (int u : adjT[v]) if (comp[u] == -1) dfs2(u, cl);
    }

    bool satisfiable() {
        for (int i = 0; i < 2*n; i++) if (!visited[i]) dfs1(i);
        reverse(order.begin(), order.end());
        for (int v : order) if (comp[v] == -1) dfs2(v, comp[v] = 0), comp[v] = 0; // fix
        // Actually need label counter
        int label = 0;
        fill(comp.begin(), comp.end(), -1);
        for (int v : order) if (comp[v] == -1) dfs2(v, label++);
        
        for (int i = 0; i < n; i++) {
            if (comp[2*i] == comp[2*i+1]) return false;
            assignment[i] = comp[2*i] > comp[2*i+1];
        }
        return true;
    }

    vector<bool> getAssignment() { return assignment; }
};

int main() {
    // Example: (x1 ∨ x2) ∧ (¬x1 ∨ x3) ∧ (¬x2 ∨ ¬x3)
    TwoSAT solver(3);
    solver.addClause(1, 2);     // x1 ∨ x2
    solver.addClause(-1, 3);    // ¬x1 ∨ x3
    solver.addClause(-2, -3);   // ¬x2 ∨ ¬x3

    if (solver.satisfiable()) {
        cout << "SATISFIABLE\n";
        for (int i = 0; i < 3; i++)
            cout << "x" << i+1 << " = " << solver.getAssignment()[i] << "\n";
    } else {
        cout << "UNSATISFIABLE\n";
    }
    return 0;
}

Complexity Analysis

• Time: O(n + m) (n = Variables, m = Clauses)
• Space: O(n + m)

ประยุกต์ใช้

• Scheduling, Planning, Circuit Verification
• Graph Coloring (2-Colorable = 2-SAT)
• Constraint Satisfaction Problems