Cook-Levin teoremi, Boole doyurulabilirlik probleminin (SAT) NP-tam olduğunu söyler. SAT, bir Boole formülünde değişkenlere doğru veya yanlış değerler verilerek formülün doğru hâle getirilip getirilemeyeceğini sorar. NP-tamlık, problemin NP sınıfında bulunması ve NP’deki her problemin polinom zamanda ona indirgenebilmesi anlamına gelir. Böylece SAT, NP problemlerinin polinom zamanlı indirgemeler açısından temel bir karşılaştırma problemidir. [1][2]
İspatın ana fikri
İspat, NP’deki herhangi bir problem için olası bir çözümü polinom zamanda doğrulayan hesabı Boole formülüne dönüştürür. Formül, hesaplamanın başlangıcını, adım adım geçişlerini ve kabul durumuna ulaşmasını kısıtlarla kodlar. Formül doyurulabiliyorsa, ilgili girdi için kabul edilen bir hesaplama vardır; kabul edilen bir hesaplama varsa, onu temsil eden formül de doyurulabilir. Dönüşümün boyutu girdi uzunluğunun polinomu ile sınırlı olduğundan, bu indirgeme polinom zamanda kurulabilir. Cook’un özgün 1971 çalışması bu genel indirgeme fikrini ortaya koymuştur. [1][3]
Tarih ve kuramsal önemi
Sonuç, Stephen Cook’un 1971’de yayımladığı çalışmayla ilişkilendirilir; Leonid Levin’in bağımsız çalışması da teoremin adında yer alır. Cook’un makalesi, NP’deki tanıma problemlerinin önermesel mantık problemlerine indirgenebileceğini gösterir. Daha sonraki ders notlarında teorem SAT’ın NP-tamlığı olarak ifade edilir; özgün makalede ise eşdeğer bir mantıksal formülasyon kullanılmıştır. [1][2][3]
Teorem, P ile NP’nin eşit olup olmadığını kanıtlamaz. SAT’ın polinom zamanda çözülebilir olması P=NP sonucunu verirdi; ancak teorem böyle bir çözüm algoritmasının varlığını göstermez. Cook-Levin sonucu, başka problemlerin NP-tamlığını kanıtlamak için kullanılabilecek bir başlangıç problemi sağlar. [2][3]