1. Revolusi Algoritmik Senyap dalam Ilmu Komputer

Buka hampir semua buku teks ilmu komputer teoretis dan Anda akan menemukan peringatan tegas: “Masalah Kepuasan Boolean (Boolean Satisfiability Problem, SAT) adalah NP-Complete. Karena kompleksitas waktu kasus terburuknya tumbuh secara eksponensial sebesar $O(2^n)$ terhadap jumlah variabel $n$, instans berukuran besar pada dasarnya tidak dapat dipecahkan secara praktis (intractable).”

Secara kombinatorial murni, argumen tersebut tampak tak terbantahkan. Sebuah formula proposisional dengan $n = 100$ variabel Boolean memiliki $2^{100} \approx 1,26 \times 10^{30}$ kemungkinan penugasan nilai kebenaran. Bahkan jika sebuah superkomputer memeriksa $10^{12}$ penugasan per detik sejak Big Bang (13,8 miliar tahun lalu), hari ini ia baru menjelajahi kurang dari $10^{-8}$ ruang pencarian. Faktanya, sekitar tahun 1990, solver SAT terbaik dunia lumpuh ketika menghadapi formula dengan hanya $100$ variabel dan $400$ klausa.

Namun di abad ke-21, praktik rekayasa mematahkan intuisi buku teks tersebut jutaan kali setiap hari. Solver SAT dan SMT industri modern — seperti MiniSat, Glucose, Lingeling, CaDiCaL, Kissat, dan Z3 dari Microsoft Research — secara rutin menyelesaikan instans verifikasi formal mikroprosesor, optimasi kompiler, dan resolusi dependensi paket yang memuat $10.000.000$ ($10^7$) variabel dan $50.000.000$ ($5 \times 10^7$) klausa hanya dalam hitungan detik.

Ketika Donald E. Knuth menerbitkan Volume 4B (Bagian 7.2.2.2) dari The Art of Computer Programming pada tahun 2015, beliau mendedikasikan lebih dari 300 halaman khusus untuk solver SAT, memuji terobosan akhir 1990-an dan awal 2000-an sebagai salah satu revolusi algoritmik terbesar dalam sejarah ilmu komputer. Jika dahulu mereduksi masalah ke SAT berarti membuktikan bahwa masalah itu mustahil diselesaikan, kini menerjemahkan masalah kombinatorial sulit ke SAT adalah strategi utama untuk menyelesaikannya secara instan.

2. Bentuk Normal Konjungtif (CNF), Transformasi Tseitin, dan Teorema Cook-Levin (1971)

2.1 Bentuk Normal Konjungtif (CNF) dan Pengodean Linear Tseitin

Sebuah solver SAT beroperasi pada formula proposisional $\Phi$ di atas $n$ variabel Boolean $V = \{x_1, \dots, x_n\}$ bernilai $\{0, 1\}$. Sebuah literal $\ell \in \{x_v, \neg x_v\}$ adalah variabel atau negasinya; sebuah klausa $C_i = \bigvee_{j=1}^{k_i} \ell_{i,j}$ adalah disjungsi (OR logis, $\lor$) dari literal-literal; dan sebuah formula dalam Bentuk Normal Konjungtif (CNF) adalah konjungsi (AND logis, $\land$) dari $m$ klausa:

Jika kita mengubah sirkuit logika sembarang menjadi CNF secara naif menggunakan hukum distributif $A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)$, ukuran formula akan meledak secara eksponensial. Pada tahun 1968, Grigori Tseitin mengatasi masalah ini melalui Transformasi Tseitin: setiap gerbang logika $g$ diberi satu variabel bantu (auxiliary variable) baru $y_g$ yang mengodekan ekuivalensi lokal $y_g \leftrightarrow \text{gate}(a, b)$ hanya dengan 3 atau 4 klausa. Misalnya, gerbang AND $y_g \leftrightarrow (a \land b)$ setara dengan tiga klausa:

Dengan demikian, sirkuit apa pun dengan $|G|$ gerbang dapat dikonversi dalam waktu dan ruang linear $O(|G|)$ menjadi formula 3-CNF yang ekuisatisfiabel (equisatisfiable).

2.2 Teorema Cook-Levin dan Jurang Kompleksitas antara 2-SAT vs. 3-SAT

Pada tahun 1971, Stephen Cook dan Leonid Levin secara independen membuktikan Teorema Cook-Levin: setiap masalah keputusan di kelas $\text{NP}$ dapat direduksi dalam waktu polinomial ke SAT dengan mengodekan tabel komputasi ruang-waktu mesin Turing nondeterministik selama $p(n)$ langkah (status $S_{t,q}$, posisi head $H_{t,i}$, simbol pita $T_{t,i,\sigma}$) sebagai formula CNF.

Ketika setiap klausa memiliki paling banyak $k$ literal ($k$-SAT), terdapat jurang tajam antara $k = 2$ dan $k = 3$:

• 2-SAT dapat diselesaikan dalam waktu linear $O(n + m)$: klausa biner $(\ell_1 \lor \ell_2)$ ekuivalen dengan dua implikasi berarah deterministik $(\neg \ell_1 \Rightarrow \ell_2) \land (\neg \ell_2 \Rightarrow \ell_1)$. Pada Graf Implikasi dengan $2n$ literal, algoritma Tarjan menemukan Komponen Terhubung Kuat (SCC) dalam waktu $O(n+m)$: formula satisfiabel jika dan hanya jika tidak ada variabel $x_v$ yang berada di SCC yang sama dengan $\neg x_v$.
• 3-SAT adalah NP-Complete: klausa terner $(\ell_1 \lor \ell_2 \lor \ell_3)$ setara dengan $(\neg \ell_1 \land \neg \ell_2) \Rightarrow \ell_3$, sebuah hiper-sisi yang membutuhkan dua premis sekaligus. Di bawah Exponential Time Hypothesis (ETH), tidak ada algoritma deterministik yang menyelesaikan 3-SAT dalam waktu subeksponensial $2^{o(n)}$ pada kasus terburuk.

3. Algoritma DPLL Klasik (1962) dan Tragedi Backtracking Kronologis

Algoritma DPLL (Davis, Putnam, Logemann, Loveland, 1962) menggabungkan pencarian mendalam (DFS) dengan Unit Propagation (Boolean Constraint Propagation, BCP):

Unit Propagation (BCP): Jika di bawah penugasan parsial saat ini semua literal dalam klausa $C = (\ell_1 \lor \dots \lor \ell_{k-1} \lor \ell_k)$ kecuali $\ell_k$ bernilai False ($0$) dan $\ell_k$ belum ditugaskan, maka $C$ disebut klausa unit (Unit Clause). Solver segera memaksa $\ell_k = \text{True}$ ($1$) tanpa percabangan, memicu efek domino propagasi unit baru hingga mencapai titik tetap atau memalsukan seluruh literal suatu klausa (Konflik).

Mengapa DPLL mentok pada kisaran 100 variabel? Karena backtracking kronologis. Jika solver menetapkan $x_1 = 0$ pada level keputusan $d = 1$, lalu membuat 48 keputusan independen pada $x_2, \dots, x_{49}$ di level $d = 2 \dots 49$, dan pada level $d = 50$ memilih $x_{50} = 1$ yang langsung memicu konflik murni akibat $x_1 = 0$ dan $x_{50}$ melalui klausa $(x_1 \lor \neg x_{50} \lor \pm x_{51})$ dan $(x_1 \lor x_{50} \lor \pm x_{52})$, DPLL buta terhadap akar masalah di level 1. Ia hanya mundur satu langkah ke level $d = 49$, membalik variabel $x_{49}$ yang tidak bersalah, dan mengulangi kegagalan yang persis sama di $2^{48} \approx 2,81 \times 10^{14}$ subpohon sia-sia (thrashing)!

4. Revolusi CDCL: Graf Implikasi, Resolusi 1-UIP, dan Backjumping Non-Kronologis

Diperkenalkan pada GRASP (Marques-Silva & Sakallah, 1996) dan disempurnakan dalam Chaff (Moskewicz et al., 2001), Conflict-Driven Clause Learning (CDCL) mengubah setiap konflik menjadi klausa baru yang dipelajari secara permanen.

  flowchart TD
    Start["Input: Formula CNF Φ (Level Keputusan d = 0)"] --> BCP["Boolean Constraint Propagation (BCP)<br/>Propagasi unit cepat melalui Two-Watched Literals (2WL)"]
    BCP --> CheckConflict{"Klausa Konflik κ<br/>Terfalsifikasi?"}
    CheckConflict -- "Tanpa Konflik" --> CheckAllAssigned{"Semua Variabel<br/>Sudah Ditugaskan?"}
    CheckAllAssigned -- "Ya" --> SAT["SATISFIABLE (SAT)<br/>Kembalikan solusi σ"]
    CheckAllAssigned -- "Tidak" --> Branch["Percabangan (Decision): d ← d + 1<br/>Pilih variabel dengan aktivitas VSIDS tertinggi<br/>Tentukan polaritas via Phase Saving"]
    Branch --> BCP
    CheckConflict -- "Ya (Konflik!)" --> CheckLevelZero{"Di Level Akar<br/>d == 0?"}
    CheckLevelZero -- "Ya" --> UNSAT["UNSATISFIABLE (UNSAT)<br/>Keluarkan sertifikat bukti DRAT"]
    CheckLevelZero -- "Tidak (d > 0)" --> Analyze["Analisis Konflik (Resolusi 1-UIP)<br/>Telusuri Graf Implikasi mundur dari κ<br/>Resolusi hingga tersisa tepat 1 literal di level d (First UIP)"]
    Analyze --> Learn["Pelajari Klausa & Bump VSIDS<br/>Tambahkan C_learned ke basis data (hitung LBD)<br/>Tingkatkan skor VSIDS variabel yang terlibat"]
    Learn --> Backjump["Backjump Non-Kronologis<br/>Lompat langsung ke Assertion Level d_back (level tertinggi ke-2 di C_learned)<br/>C_learned langsung aktif sebagai Klausa Unit di BCP!"]
    Backjump --> BCP

4.1 Graf Implikasi, Resolusi Boolean, dan First Unique Implication Point (1-UIP)

Setiap literal yang ditugaskan $\ell@d$ mencatat level keputusan $d$ dan klausa alasan (antecedent / reason clause) $\text{reason}(\ell)$. Saat klausa konflik $\kappa$ terfalsifikasi, CDCL menginisialisasi $C \leftarrow \kappa$ dan berjalan mundur mengikuti Trail pada level saat ini $d_{\text{curr}}$, menerapkan aturan Resolusi Boolean secara berulang:

Pada graf implikasi, sebuah simpul $u@d_{\text{curr}}$ adalah Unique Implication Point (UIP) jika setiap jalur berarah dari keputusan $\ell_{\text{dec}}@d_{\text{curr}}$ menuju simpul konflik $\Lambda$ wajib melewati $u$ (dominator). UIP yang paling dekat dengan konflik disebut First UIP (1-UIP), yang tercapai tepat pada saat klausa kerja $C$ hanya menyisakan satu literal saja dari level keputusan saat ini $d_{\text{curr}}$!

Dengan $x_1 = 0@1, x_2 = 0@2, x_3 = 1@3$, keputusan $x_4 = 1@5$, serta klausa $\omega_1 = (x_1 \lor \neg x_4 \lor x_5)$, $\omega_2 = (\neg x_4 \lor \neg x_5 \lor x_6)$, $\omega_3 = (x_2 \lor \neg x_6 \lor x_7)$, $\omega_4 = (\neg x_3 \lor \neg x_6 \lor x_8)$ yang berujung pada konflik $\kappa = (\neg x_7 \lor \neg x_8)$, dua langkah resolusi $\kappa$ dengan $\omega_4$ (pivot $x_8$) dan $\omega_3$ (pivot $x_7$) langsung menghasilkan klausa terpelajar 1-UIP:

4.2 Backjumping Non-Kronologis dan Assertion Level

Karena level dalam $C_{\text{learned}}$ adalah $\{5, 3, 2\}$, solver melompat langsung ke level keputusan tertinggi kedua (Assertion Level) $d_{\text{back}} = 3$! Di level $3$, $x_2@2$ dan $\neg x_3@3$ masih bernilai False sedangkan $\neg x_6$ kembali bebas, sehingga $C_{\text{learned}}$ langsung bertindak sebagai klausa unit penegas (asserting clause) dan memaksa $\neg x_6 = 1@3$ ($x_6 = 0@3$) melalui BCP!

5. Keajaiban Rekayasa: Two-Watched Literals (2WL), VSIDS, dan LBD

1. Two-Watched Literals (2WL, Chaff 2001): Selama sebuah klausa memiliki sedikitnya dua literal yang belum bernilai False, klausa tersebut tidak mungkin menjadi klausa unit maupun konflik. Solver hanya memantau dua literal $w_1, w_2$ per klausa. Keajaiban terbesarnya terjadi saat backjumping: membatalkan penugasan variabel secara otomatis mempertahankan invarian 2WL, sehingga backtracking membutuhkan tepat nol pembaruan pointer ($O(1)$)!
2. VSIDS (Variable State Independent Decaying Sum) & Phase Saving: Setiap variabel yang terlibat dalam resolusi konflik mendapat tambahan skor $+\Delta$, sementara $\Delta \leftarrow \Delta / \gamma$ ($\gamma = 0,95$) membesar setiap kali terjadi konflik, memfokuskan pencarian pada titik kemacetan terbaru.
3. LBD (Literal Block Distance / Klausa «Glue») & Rapid Restarts: Glucose (Audemard & Simon, 2009) mendefinisikan $\text{LBD}(C)$ sebagai jumlah level keputusan berbeda dalam klausa $C$. Klausa dengan $\text{LBD} = 2$ (Glue Clauses) mengikat UIP saat ini langsung ke satu blok keputusan masa lalu dan disimpan secara permanen.

6. Implementasi Lengkap Mesin Inti CDCL dalam Python

Berikut adalah implementasi lengkap dan mandiri dari solver CDCL dalam bahasa Python yang mencakup BCP, graf implikasi, resolusi 1-UIP, backjumping non-kronologis, dan VSIDS:

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112

from typing import List, Dict, Optional, Set, Tuple

class CDCLSolver:
    '''Minimal Conflict-Driven Clause Learning (CDCL) SAT Solver with 1-UIP & VSIDS.'''
    def __init__(self, num_vars: int, clauses: List[List[int]]):
        self.num_vars = num_vars
        self.clauses: List[List[int]] = [list(set(c)) for c in clauses]
        self.assigns: Dict[int, bool] = {}
        self.trail: List[int] = []
        self.level: Dict[int, int] = {}
        self.reason: Dict[int, Optional[List[int]]] = {}
        self.decision_level: int = 0
        self.activity: Dict[int, float] = {v: 0.0 for v in range(1, num_vars + 1)}
        for c in self.clauses:
            for lit in c:
                self.activity[abs(lit)] += 1.0
        self.var_inc: float = 1.0
        self.var_decay: float = 0.95

    def value_lit(self, lit: int) -> Optional[bool]:
        var = abs(lit)
        if var not in self.assigns:
            return None
        return self.assigns[var] if lit > 0 else not self.assigns[var]

    def assign(self, lit: int, level: int, reason: Optional[List[int]]) -> None:
        var = abs(lit)
        self.assigns[var] = (lit > 0)
        self.trail.append(lit)
        self.level[var] = level
        self.reason[var] = reason

    def bcp(self) -> Optional[List[int]]:
        changed = True
        while changed:
            changed = False
            for clause in self.clauses:
                unassigned_lit = None
                num_unassigned = 0
                satisfied = False
                for lit in clause:
                    val = self.value_lit(lit)
                    if val is True:
                        satisfied = True
                        break
                    elif val is None:
                        num_unassigned += 1
                        unassigned_lit = lit
                if satisfied:
                    continue
                if num_unassigned == 0:
                    return clause
                if num_unassigned == 1 and unassigned_lit is not None:
                    self.assign(unassigned_lit, self.decision_level, clause)
                    changed = True
        return None

    def analyze_conflict(self, conflict_clause: List[int]) -> Tuple[List[int], int]:
        learned: Set[int] = set(conflict_clause)
        def count_curr_level(cset: Set[int]) -> int:
            return sum(1 for lit in cset if self.level[abs(lit)] == self.decision_level)

        idx = len(self.trail) - 1
        while count_curr_level(learned) > 1:
            while True:
                pivot_lit = self.trail[idx]
                idx -= 1
                if -pivot_lit in learned and self.level[abs(pivot_lit)] == self.decision_level:
                    break
            pivot_var = abs(pivot_lit)
            antecedent = self.reason[pivot_var]
            assert antecedent is not None
            self.activity[pivot_var] += self.var_inc
            learned.remove(-pivot_lit)
            for lit in antecedent:
                if lit != pivot_lit:
                    learned.add(lit)

        learned_clause = list(learned)
        for lit in learned_clause:
            self.activity[abs(lit)] += self.var_inc
        self.var_inc /= self.var_decay
        levels = sorted({self.level[abs(lit)] for lit in learned_clause}, reverse=True)
        backjump_level = levels[1] if len(levels) > 1 else 0
        return learned_clause, backjump_level

    def backtrack(self, target_level: int) -> None:
        while self.trail and self.level[abs(self.trail[-1])] > target_level:
            lit = self.trail.pop()
            var = abs(lit)
            del self.assigns[var], self.level[var], self.reason[var]
        self.decision_level = target_level

    def solve(self) -> Tuple[bool, Optional[Dict[int, bool]]]:
        if self.bcp() is not None:
            return False, None
        while True:
            unassigned = [v for v in range(1, self.num_vars + 1) if v not in self.assigns]
            if not unassigned:
                return True, dict(self.assigns)
            branch_var = max(unassigned, key=lambda v: self.activity[v])
            self.decision_level += 1
            self.assign(branch_var, self.decision_level, reason=None)
            while True:
                conflict = self.bcp()
                if conflict is None:
                    break
                if self.decision_level == 0:
                    return False, None
                learned_clause, backjump_level = self.analyze_conflict(conflict)
                self.clauses.append(learned_clause)
                self.backtrack(backjump_level)

7. Fisika Statistik dan Transisi Fase $k$-SAT Acak ($\alpha_c \approx 4,267$)

Untuk formula 3-SAT acak dengan $n$ variabel dan $m = \alpha n$ klausa (rasio kepadatan klausa terhadap variabel $\alpha = m / n$), metode momen pertama memberikan ekspektasi jumlah solusi $\mathbb{E}[Z]$:

Menggunakan Metode Rongga (Cavity Method) dan One-Step Replica Symmetry Breaking (1RSB) dari fisika kaca spin (spin glass), Mézard, Parisi, dan Zecchina (2002) menemukan ambang batas kritis sejati untuk 3-SAT acak:

  flowchart TD
    subgraph PhaseTransition["Transisi Fase 3-SAT Acak Berdasarkan Kepadatan α = m/n"]
        S1["1. Fase Cair Under-Constrained (α < 3,86 : Easy-SAT)<br/>• Solusi membentuk satu klaster raksasa yang saling terhubung di {0,1}^n<br/>• Diselesaikan dengan cepat dalam waktu polinomial"]
        S2["2. Fase Kaca Pecah & Membeku (3,86 < α < 4,267 : Hard-SAT)<br/>• Pada α_d ≈ 3,86 (transisi 1RSB), ruang solusi hancur menjadi pulau-pulau terisolasi!<br/>• Pada α_f ≈ 4,254 variabel di dalam tiap klaster membeku secara kaku (Freezing)"]
        S3["3. Ambang Kritis Satisfiability (α_c ≈ 4,267 : Puncak Kesulitan Eksponensial)<br/>• Probabilitas SAT jatuh tajam dari 1 ke 0<br/>• Setiap bukti resolusi membutuhkan panjang eksponensial 2^Ω(n) (Chvátal–Szemerédi)"]
        S4["4. Fase Over-Constrained (α > 4,267 : Easy-UNSAT)<br/>• Kepadatan klausa tinggi langsung memicu kontradiksi di kedalaman dangkal<br/>• Ukuran bukti menyusut saat α membesar"]
    end
    S1 -->|"α_d ≈ 3,86 (Shattering)"| S2
    S2 -->|"α_c ≈ 4,267 (Transisi UNSAT)"| S3
    S3 -->|"α > 4,267 (Konflik Dangkal)"| S4

Pada $\alpha_c \approx 4,267$, hipergraf acak bersifat graf ekspander tanpa leher botol lokal sehingga setiap bukti resolusi wajib berukuran eksponensial $2^{\Omega(n)}$ (Chvátal & Szemerédi, 1988). Sebaliknya, masalah industri nyata memiliki struktur komunitas modular (Community Structure) dan himpunan Backdoor kecil (Ansótegui et al. 2012; Williams, Gomes, Selman 2003), yang dieksploitasi oleh CDCL untuk memecahkan 10 juta variabel dalam hitungan detik.

8. Kejayaan di Dunia Nyata dan Bukti Matematika 200 Terabyte

1. Matematika Berbantuan Komputer & Bukti DRAT 200 TB (Heule, Kullmann, Marek 2016): Menggunakan Cube-and-Conquer pada 800 core, mereka membuktikan bahwa Masalah Tripel Pythagoras Boolean ($a^2 + b^2 = c^2$) dapat dipenuhi hingga $N = 7824$ (SAT), tetapi mustahil pada $N = 7825$ (UNSAT), menghasilkan sertifikat bukti formal DRAT sebesar 200 Terabyte, serta menyelesaikan bilangan Schur $S(5) = 160$ (2018) dan konjektur Keller dimensi 7 (2020).
2. Verifikasi Formal Cip EDA (CEC & BMC): sirkuit Miter (XOR antara spesifikasi RTL dan gerbang logika) diverifikasi dengan solver SAT sebelum produksi setiap prosesor modern.
3. Manajer Paket (Debian apt, Rust Cargo, Dart PubGrub, uv) dan Solver SMT ($\text{DPLL}(T)$: Z3 & cvc5): menggabungkan inti CDCL dengan solver teori orde pertama untuk menggerakkan eksekusi simbolik dan mesin keamanan cloud AWS Zelkova.