SAT Problemi: Mantığın İlk NP-Tam Problemi ve Modern Çözücü Mucizesi

Bir mantık bulmacası

Üç ifadeden oluşan bir formül düşünün:

$(x_1 \lor x_2 \lor \lnot x_3) \land (\lnot x_1 \lor x_3 \lor x_4) \land (x_2 \lor \lnot x_4)$

Burada $x_i$'ler boolean değişkenler (TRUE/FALSE). Soru: bu formülü TRUE yapan bir atama var mı?

Bu durumda evet — örneğin $x_1 = T, x_2 = T, x_3 = T, x_4 = T$ tüm üç ifadeyi sağlar. Ama "var mı yok mu?" sorusu genel olarak ne kadar zor?

Bu, Boolean Satisfiability (SAT) problemidir. Modern bilgisayar bilimi ve mantık teorisinin merkezi.

Tanım — CNF formu

SAT problemi: Verilen bir önerme mantığı formülü, onu TRUE yapan değişken ataması var mı?

Genellikle Konjüktif Normal Form (CNF):

• Literal = bir değişken veya tersi: $x_i$ veya $\lnot x_i$.
• Cümle = literallerin veya (OR) ile birleşimi: $(x_1 \lor \lnot x_2 \lor x_3)$.
• CNF formülü = cümlelerin ve (AND) ile birleşimi.

3-SAT = her cümlede tam 3 literal olan SAT.

Cook-Levin teoremi (1971-73)

Stephen Cook (1971, ABD) ve bağımsız olarak Leonid Levin (1973, SSCB) — soğuk savaş döneminin paralel keşfi:

SAT problemi NP-tamdır.

Bu cümlenin anlamı:

1. SAT, NP sınıfındadır (bir atama verilirse, polinom zamanda doğrulanabilir).
2. NP'deki her problem SAT'a polinom zamanda indirgenebilir (reduction).

Dolayısıyla SAT'ı polinom zamanda çözen bir algoritma bulursak, tüm NP problemlerini polinom zamanda çözeriz → P = NP.

Cook-Levin teoremi, NP-tamlık kavramının doğum belgesi. Sonra Karp (1972) 21 ek NP-tam problem buldu (Hamilton döngüsü, gezgin satıcı, knapsack, vs.). Bugün binlerce NP-tam problem biliniyor.

Neden bu kadar önemli?

NP-tam problemler eşdeğer: birini polinom çözerseniz hepsini çözersiniz. Onlar hesaplamalı karmaşıklığın kalbi.

Ve SAT onların referans noktasıdır: bir problem NP'de mi diye sormak için, "SAT'a indirgeyebilir miyim?" sorusunu sorarız.

Trivial üst sınır: $O(2^n)$

$n$ değişken varsa $2^n$ farklı atama var. Hepsini deneyip kontrol et. Bu brute force üstel.

20 değişken: $2^{20} \approx 10^6$ — kolay.
40 değişken: $2^{40} \approx 10^{12}$ — yavaş.
80 değişken: $2^{80} \approx 10^{24}$ — imkansız.

Polinom algoritma bulunamamıştır (P=NP açık). Ama pratikte SAT problem boyutu milyonları geçti! Bu nasıl?

DPLL algoritması (1962)

Davis-Putnam-Logemann-Loveland: SAT için akıllı tarama algoritması.

1. Değişken seç, TRUE atayın.
2. Cümleleri sadeleştir: TRUE literal varsa cümleyi at; FALSE literal varsa cümleden at.
3. Tek-literal cümle (unit clause) varsa, o literali zorla doğru kabul et.
4. Hiç değişken kalmazsa ve cümleler sağlandıysa, çözüldü.
5. Boş cümle varsa (FALSE), geri dön (backtrack), aksini dene.

Bu, bilinçli üstel algoritma. Pratikte çoğunlukla küçük bir kısmı tarar.

CDCL — modern devrim (1996+)

Conflict-Driven Clause Learning — DPLL'in modern halefi. Marques-Silva ve Sakallah (GRASP, 1996) tanıttı.

Fikir: çakışma yaşandığında, çakışmadan öğren ve yeni bir engel cümle (learned clause) ekleyerek aynı yanlışı bir daha yapmamayı garanti et.

Bu basit fikir SAT'ı mucize yaptı:

• 1990'lar: birkaç bin değişken sınırı.
• 2024: 10 milyon değişken rutin olarak çözülüyor.

Yıllık SAT Yarışmaları modern çözücülerin performansını takip ediyor: Kissat, CaDiCaL, MiniSAT gibi açık kaynak araçlar dünya standartı.

SAT uygulamaları — şaşırtıcı yelpaze

1. Donanım doğrulama

Bir mikroişlemcinin doğru çalıştığını ispatlamak için — milyarlarca senaryo. SAT çözücü kullanılır.

• Intel ve AMD her yeni çip için SAT çözücü çalıştırır.
• Pentium FDIV bug (1994) tipi hataları önler.

2. Yazılım doğrulama

Bir kodun bir özelliği sağladığını formal olarak ispatla. SAT (ve SMT — SAT modulo theories) çözücüler bug avı için temel.

• Microsoft SLAM projesi: Windows driver doğrulama.
• Linux kernel verification: model checker'lar.

3. AI Planlama

Bir robotun belirli adımlarla hedefe ulaşması nasıl yapılır? SAT problemi olarak modellenip çözülür.

4. Cryptography saldırıları

Bazı şifreleme zayıflıklarını SAT olarak modelleyip kırma.

5. Sudoku çözücü

Sudoku problemleri SAT olarak formüle edilip 1 saniyenin altında çözülür.

6. Tabular planlama

Üniversite ders programları, hastane vardiya planları, vs. SAT problemi olarak modellenir.

Cook ile Levin — paralel keşif

İki bağımsız keşif. Stephen Cook (Toronto, 1971) İngilizce yayımladı; Leonid Levin (SSCB, 1973) Rusça yayımladı.

Levin'in makalesi sansür ve gecikme nedeniyle Batı dünyasında geç tanındı. Bugün Cook-Levin teoremi ortak isim ile anılır.

Cook Turing Ödülü (1982) aldı. Levin de uluslararası kabule sahip olmasına rağmen ödül almadı (politik nedenler dahil). Tarihsel haksızlıkların bir başka örneği.

Modern SAT çözücülerinin gizemi

NP-tam olan bir problem, pratikte çözülüyor? Niçin?

Açıklamalar:

• Endüstri formülleri rastgele değil, yapısal (donanım, yazılım). Düzensiz örüntülere göre daha kolay.
• CDCL bu yapısal örüntüleri öğrenip kestirme yollar bulur.
• Heuristik değişken seçimi: VSIDS, jeroslow-wang, vs.
• Random restarts ve clause minimization.

P=NP açık olsa bile, pratikte SAT çoğunlukla çözülebiliyor. Bu, karmaşıklık teorisi ile mühendislik arasındaki ilginç fark.

Açık problemler

• 3-SAT polinom zamanda çözülebilir mi? (= P vs NP).
• SAT için her problem instance üstel midir? (Exponential Time Hypothesis, ETH).
• MaxSAT, #SAT (sayma) — bunlar SAT'ten daha zordur.

Sonuç

SAT problemi:

• Modern karmaşıklık teorisinin temeli (Cook-Levin 1971).
• Pratik mucize: NP-tam ama 10M değişken çözülüyor.
• Şifreleme, donanım, yazılım, AI'da rutin araç.
• Açık matematik soruları (P=NP, ETH) için referans noktası.

Bir mantık bulmacasından — boolean değişkenlerin atanması — modern bilgisayar bilimi karmaşıklık teorisinin ana karakteri. Cook 1971'de bir sayfada yazdı; Levin SSCB'de bağımsız buldu. 53 yıl sonra her ana mikroişlemcinin doğrulamasında, her büyük yazılım'ın güvenlik testinde SAT çalışıyor.

Mantık ile mühendislik arasındaki en derin köprü, belki de matematik tarihinin en pratik soyut sonucu.