庫克-李文定理

庫克-李文定理（英語：Cook–Levin theorem）或者庫克定理（英語：Cook's theorem）是有關計算複雜度理論的一個定理。它證明了布爾可滿足性問題（SAT問題）是NP完全問題。即：

1. 「一個布爾方程式是否存在解」這個問題本身是一個NP問題；
2. 任何其他NP問題都可以在多項式時間內被一決定型圖靈機歸約成這個問題。

庫克-李文定理是以史蒂芬·庫克和利奧尼德·李文為名。

這定理一個非常重要的推論為：如果SAT問題可在多項式時間內被一確定型演算法解決，則「所有的」NP問題都存在可在多項式時間內解決之的確定型演算法。因此，有關以上這個演算法存在與否的問題等價於P/NP問題——現代的理論電腦科學中最重要的未解問題之一。

定義

對於一個決定性問題，如果我們可以使用非決定型圖靈機在多項式時間之內解決它，我們稱它「在NP內」。

一個「布爾可滿足性問題的成員（instance）」是一個布爾表達式，或者說，一些布爾變數跟布爾邏輯運算符的組合。

對於一個表達式，如果存在某些給予布爾變數真值的方式使得這個表達式的值為真，我們稱它「可滿足的」。

概念

給定任何NP的決定性問題，建立一個可以在多項式時間內解決此問題的非決定型圖靈機。然後，對每個輸入，建立一個布爾表示式，告訴我們這個輸入進去「是否會正確運作，停止，並且回傳答案為真」。那麼，這個表示式就是可滿足的，若且唯若這個機器正確的跑完這個輸入，並且會停止，回答這個輸入是正確的。這樣，問題「這個我們建立的表示式是否可滿足」，與問題「這個圖靈機是否會回傳"真"」就會變成等價的問題。

結果

這個定理的證明展現了任何NP問題都可以在多項式時間內歸約成（另外事實上，只需要對數空間）轉換成一個布爾可滿足性問題。這代表如果布爾可滿足性問題可以用圖靈機在多項式時間內解決，那麼所有NP內的問題都可以在多項式時間內解決，因此複雜度類NP就會等於複雜度類P。

NP完全的重要性在1972年因為理察·卡普的論文《組合問題之間的可還原性》而清楚的表現出來。裡面列出了二十一個有關組合和圖論的問題（卡普的二十一個NP-完全問題），證明裡面的每個均因為其難以解決而惡名昭彰的問題都是NP完全。

貢獻

NP完全的概念是在1960年代晚期和1970年代初期，被北美和蘇聯的研究者於同一時期分別建立起來的。在1971年的美國，史蒂芬·庫克發表了他的論文《定理證明程式的複雜性》於新成立的ACM計算理論研討會內。理察·卡普接續的論文《組合問題之間的可還原性》則藉由提出了二十一個NP-完全問題的列表，讓庫克之前的論文重新受到了注意。庫克和卡普因為這個成就得到了圖靈獎。

西奧多·P·貝克（Theodore P. Baker）、約翰·吉爾（John Gill）和羅伯特·M·索洛維於1975年證明了使用諭示機模型解決NP-問題需要指數時間，因此對於NP-完備性的興趣又再次被提高。

在蘇聯，德赫蒂亞（M. Dekhtiar）於1969年發表了與貝克、吉爾和索洛維等同的研究。過後利奧尼德·李文的論文《通用搜尋型問題》翻譯過後出版於1973年。不過在更早的幾年之前，這論文的內容就有在演講中提到並且付印過。

李文的研究與庫克和卡普些微的不同，在於他考慮的議題專注在搜尋型問題。這類問題不僅僅是找到解答存在與否，還必須要輸出解答。他提出了六個NP-完全的搜尋型問題，並且還附加證明了一個能在最佳時間內解決這問題的演算法。