sat3_dpll.cpp

// sat3_dpll.cpp
// -----------------------------------------------------------------
// 3-SAT：暴力枚舉 vs. DPLL（單元傳播 + 純文字消去 + 回溯）
//
// 文字編碼：變數 v（1 起算）的正文字 = +v，負文字 = -v。
// 子句 = 文字的 vector；公式 = 子句的 vector（CNF）。
//
// Compile: g++ -std=c++17 -O2 -Wall -Wextra -o sat3_dpll sat3_dpll.cpp
// -----------------------------------------------------------------
#include <iostream>
#include <vector>
#include <algorithm>
#include <random>
#include <chrono>
#include <cmath>

using namespace std;

using Clause  = vector<int>;
using Formula = vector<Clause>;

// ---------- 共用：檢驗一組完整賦值是否滿足公式 ----------
bool satisfies(const Formula& f, const vector<int>& assign) {
    for (const auto& cl : f) {
        bool ok = false;
        for (int lit : cl) {
            int v = abs(lit);
            if ((lit > 0 && assign[v] == 1) || (lit < 0 && assign[v] == -1)) {
                ok = true; break;
            }
        }
        if (!ok) return false;
    }
    return true;
}

// ---------- 方法一：暴力枚舉 O(2^n · m) ----------
bool bruteForceSAT(const Formula& f, int numVars, vector<int>& model) {
    for (long long mask = 0; mask < (1LL << numVars); ++mask) {
        vector<int> assign(numVars + 1);
        for (int v = 1; v <= numVars; ++v)
            assign[v] = (mask >> (v - 1)) & 1 ? 1 : -1;
        if (satisfies(f, assign)) { model = assign; return true; }
    }
    return false;
}

// ---------- 方法二：DPLL ----------
class DPLL {
public:
    long long nodes = 0;                 // 統計：拜訪的搜尋節點數
    vector<int> model;

    bool solve(int numVars, const Formula& f) {
        nodes = 0;
        return dfs(f, vector<int>(numVars + 1, 0));
    }
private:
    // 化簡公式：刪掉已滿足子句、刪掉為假的文字
    // 回傳 false 表示出現空子句（矛盾）
    static bool simplify(const Formula& in, const vector<int>& assign,
                         Formula& out) {
        out.clear();
        for (const auto& cl : in) {
            Clause reduced;
            bool sat = false;
            for (int lit : cl) {
                int v = abs(lit), want = lit > 0 ? 1 : -1;
                if (assign[v] == want) { sat = true; break; }
                if (assign[v] == 0) reduced.push_back(lit);
            }
            if (sat) continue;
            if (reduced.empty()) return false;   // 空子句
            out.push_back(reduced);
        }
        return true;
    }

    bool dfs(Formula f, vector<int> assign) {
        ++nodes;
        // 1. 單元傳播：只剩一個文字的子句 -> 強制賦值
        bool changed = true;
        while (changed) {
            changed = false;
            Formula g;
            if (!simplify(f, assign, g)) return false;
            f = std::move(g);
            if (f.empty()) { model = assign; return true; }
            for (const auto& cl : f)
                if (cl.size() == 1) {
                    int lit = cl[0];
                    assign[abs(lit)] = lit > 0 ? 1 : -1;
                    changed = true;
                    break;
                }
        }
        // 2. 純文字消去：某變數只以單一極性出現 -> 直接滿足它
        {
            vector<int> polarity(assign.size(), 0);  // 0未見 1正 -1負 2混合
            for (const auto& cl : f)
                for (int lit : cl) {
                    int v = abs(lit), p = lit > 0 ? 1 : -1;
                    if (polarity[v] == 0) polarity[v] = p;
                    else if (polarity[v] != p) polarity[v] = 2;
                }
            for (int v = 1; v < (int)assign.size(); ++v)
                if (assign[v] == 0 && (polarity[v] == 1 || polarity[v] == -1)) {
                    assign[v] = polarity[v];
                    return dfs(f, assign);           // 化簡後重來
                }
        }
        // 3. 分支：挑出現次數最多的變數（簡單啟發）
        {
            vector<int> cnt(assign.size(), 0);
            for (const auto& cl : f)
                for (int lit : cl)
                    if (assign[abs(lit)] == 0) ++cnt[abs(lit)];
            int best = -1;
            for (int v = 1; v < (int)assign.size(); ++v)
                if (cnt[v] > 0 && (best == -1 || cnt[v] > cnt[best])) best = v;
            if (best == -1) { model = assign; return true; }
            for (int val : {1, -1}) {
                auto a2 = assign;
                a2[best] = val;
                if (dfs(f, a2)) return true;
            }
            return false;
        }
    }
};

// ---------- 隨機 3-SAT 產生器 ----------
Formula random3SAT(int numVars, int numClauses, mt19937& rng) {
    Formula f;
    uniform_int_distribution<int> var(1, numVars), sign(0, 1);
    for (int i = 0; i < numClauses; ++i) {
        Clause cl;
        while ((int)cl.size() < 3) {
            int v = var(rng);
            bool dup = false;
            for (int lit : cl) if (abs(lit) == v) dup = true;
            if (!dup) cl.push_back(sign(rng) ? v : -v);
        }
        f.push_back(cl);
    }
    return f;
}

static void printModel(const vector<int>& m, int n) {
    for (int v = 1; v <= n; ++v)
        cout << " x" << v << "=" << (m[v] == 1 ? 1 : 0);
}

int main() {
    // ---- 範例 1：可滿足的小公式 ----
    // (x1 v x2 v x3) & (~x1 v ~x2 v x3) & (x1 v ~x2 v ~x3) & (~x1 v x2 v ~x3)
    cout << "=== Example 1: hand-crafted 3-SAT (satisfiable) ===\n";
    Formula f1 = {{1,2,3},{-1,-2,3},{1,-2,-3},{-1,2,-3}};
    vector<int> m1;
    bool b1 = bruteForceSAT(f1, 3, m1);
    cout << "brute force: " << (b1 ? "SAT, model:" : "UNSAT");
    if (b1) printModel(m1, 3);
    cout << "\n";
    DPLL d1;
    bool s1 = d1.solve(3, f1);
    cout << "DPLL       : " << (s1 ? "SAT, model:" : "UNSAT");
    if (s1) printModel(d1.model, 3);
    cout << "  (nodes=" << d1.nodes << ")\n\n";

    // ---- 範例 2：不可滿足（8 個子句覆蓋 x1,x2,x3 全部組合） ----
    cout << "=== Example 2: all 8 clauses on 3 vars (unsatisfiable) ===\n";
    Formula f2;
    for (int mask = 0; mask < 8; ++mask) {
        Clause cl;
        for (int v = 1; v <= 3; ++v)
            cl.push_back((mask >> (v - 1)) & 1 ? v : -v);
        f2.push_back(cl);
    }
    DPLL d2;
    cout << "DPLL: " << (d2.solve(3, f2) ? "SAT" : "UNSAT")
         << "  (nodes=" << d2.nodes << ")\n\n";

    // ---- 範例 3：隨機 3-SAT，比較暴力與 DPLL 的節點/時間 ----
    cout << "=== Example 3: random 3-SAT, brute force vs DPLL ===\n";
    mt19937 rng(20260724);
    for (int n : {16, 20}) {
        int m = (int)llround(4.0 * n);          // 子句/變數比 4.0（接近相變 4.27）
        Formula f = random3SAT(n, m, rng);
        auto t0 = chrono::steady_clock::now();
        vector<int> bm;
        bool bb = bruteForceSAT(f, n, bm);
        auto t1 = chrono::steady_clock::now();
        DPLL dd;
        bool ds = dd.solve(n, f);
        auto t2 = chrono::steady_clock::now();
        double bruteMs = chrono::duration<double, milli>(t1 - t0).count();
        double dpllMs  = chrono::duration<double, milli>(t2 - t1).count();
        cout << "n=" << n << " m=" << m
             << " | brute: " << (bb ? "SAT" : "UNSAT")
             << " " << bruteMs << " ms"
             << " | DPLL: " << (ds ? "SAT" : "UNSAT")
             << " " << dpllMs << " ms, nodes=" << dd.nodes;
        cout << " | agree=" << (bb == ds ? "yes" : "NO!") << "\n";
        if (ds && !satisfies(f, dd.model)) cout << "  ERROR: bad model!\n";
    }

    // ---- 範例 4：相變現象觀察（m/n 從 3.0 到 5.5） ----
    cout << "\n=== Example 4: phase transition (fraction SAT over 40 trials) ===\n";
    int n = 24;
    for (double ratio : {3.0, 3.5, 4.0, 4.27, 4.5, 5.0, 5.5}) {
        int satCount = 0, trials = 40;
        long long totalNodes = 0;
        for (int t = 0; t < trials; ++t) {
            Formula f = random3SAT(n, (int)llround(ratio * n), rng);
            DPLL dd;
            if (dd.solve(n, f)) ++satCount;
            totalNodes += dd.nodes;
        }
        cout << "m/n=" << ratio << "  SAT rate=" << satCount << "/" << trials
             << "  avg nodes=" << totalNodes / trials << "\n";
    }
    return 0;
}