משפט קוק-לוין

משפט קוק-לוין הוא משפט יסודי בתורת הסיבוכיות, הקובע שהבעיה SAT היא NP-שלמה. את המשפט הוכיחו, באופן בלתי תלוי, סטפן קוק בשנת 1971, ולאוניד לוין בשנת 1973.

==מבוא==
במדעי המחשב התאורטיים יש חשיבות מרכזית לבעיות שניתן למצוא להן פתרון בזמן סביר (הגדרתו המדויקת של המושג "זמן סביר" היא טכנית, ומסתמכת על הגדרת המושג של מכונת טיורינג). אוסף הבעיות שניתן למצוא להן פתרון בזמן סביר מסומן על ידי האות P.

בנוסף לבעיות שניתן למצוא עבורן פתרון בזמן סביר, קיימות גם בעיות שניתן לבדוק בזמן סביר האם פתרון מוצע כלשהו עבורן הוא אכן פתרון לבעיה. בעיות אלו מסומנות על ידי NP. זהו אוסף בעיות שככל הנראה גדול יותר מאוסף הבעיות P, שכן קיימות בעיות רבות שידוע כיצד לבדוק בזמן סביר אם פתרון מוצע אכן פותר אותן, אך לא ידועה דרך למצוא פתרון שכזה בזמן סביר. דוגמה לבעיה מסוג זה היא השאלה האם ניתן לחלק קבוצת מספרים נתונה לשתי קבוצות, כך שסכום המספרים בקבוצה האחת יהיה שווה לסכומם בקבוצה השנייה. בהינתן חלוקה של קבוצת מספרים לשתי קבוצות, קל לבדוק האם הסכומים בשתיהן אכן שווים. אבל אם לא נתונה חלוקה כזו, קשה מאוד למצוא האם היא אכן קיימת.

כיום עדיין לא ידוע האם עבור כל בעיה שניתן לבדוק פתרון מוצע לה בזמן סביר, ניתן גם למצוא פתרון שכזה בזמן סביר. השאלה האם הדבר אפשרי מכונה בשם בעיית P=NP, כלומר האם שתי המחלקות P ו-NP שוות זו לזו, וזוהי אחת מהשאלות המרכזיות במדעי המחשב. הדעה הרווחת היא כי הדבר אינו נכון.

משפט קוק-לוין עוסק באחת מהבעיות הנמצאות ב-NP, ונקראת בעיית SAT (הגדרתה המדויקת של בעיה זו קשורה ללוגיקה מתמטית ואף כי אינה מסובכת היא טכנית למדי). המשפט אומר כי SAT שייכת לאוסף הבעיות הקשות ביותר שב-NP, במובן זה שאם תתגלה דרך למצוא פתרון בזמן סביר עבור SAT, ניתן יהיה לפתור בזמן סביר כל בעיה השייכת ל-NP. במילים אחרות, אם יתגלה פתרון בזמן סביר עבור SAT, הדבר יהווה הוכחה לכך ש-P=NP. בעיות שניחנות בתכונת קושי שכזו מכונות NP-שלמות. לכן, בניסוח מדויק יותר, משפט קוק-לוין אומר כי SAT היא בעיה NP-שלמה.

חשיבותו של משפט קוק-לוין אינה רק בתכונה של SAT שעולה ממנו, אלא גם בכך שהוא מאפשר להוכיח בקלות עבור בעיות רבות נוספות שגם הן NP-שלמות. במקום שיהיה צורך בהוכחה ישירה עבור כל אחת ואחת מהן, ניתן להשתמש בכך שידוע כי SAT היא NP-שלמה כדי להוכיח שהן NP-שלמות בעצמן בקלות רבה יותר: אם A היא בעיה שרוצים להוכיח כי היא NP-שלמה, די להראות כי ניתן לפתור את SAT בזמן יעיל אם A ניתנת לפתרון בזמן יעיל, כדי להוכיח כי גם A היא NP-שלמה.

==תיאור פורמלי==
קוק הגדיר את המושג של בעיה NP-שלמה כבעיה המקיימת שני תנאים:
# הבעיה שייכת למחלקת הסיבוכיות NP.
# כל בעיה אחרת שהיא במחלקת הסיבוכיות NP, ניתנת לרדוקציה פולינומית אליה.

בצורה פורמלית ניתן להסתכל על בעיות הכרעה כבעיות של זיהוי שפה פורמלית. כך ניתן לנסח את בעיית SAT בתור הבעיה של זיהוי השפה הבאה: שפת כל הפסוקים הלוגיים בצורת CNF (כלומר בצורה קנונית קוניוקטיבית), שישנה השמה המספקת אותם. בלוגיקה מתמטית, פסוק של תחשיב פסוקים נחשב בעל השמה מספקת אם ישנה הצבה כלשהי של ערכי אמת במשתנים שלו, כך שהפסוק מקבל ערך אמת.

משפט קוק אומר כי בעיית זיהוי שפה זו היא NP-שלמה.

משמעות המשפט היא שאם ניתן לפתור את SAT בזמן ריצה פולינומי (כלומר באופן יעיל), אז ניתן להכריע את כל הבעיות שבמחלקת הסיבוכיות NP בזמן פולינומי, דבר שיגרור את השוויון P=NP.

ההוכחה פתחה פתח להוכחה מיידית כי עשרות בעיות אחרות הן NP-שלמות (בפרט מפורסם המאמר על 21 הבעיות ה-NP שלמות של קארפ מאת ריצ'רד קארפ שפורסם שנה אחרי משפט קוק). על עבודתו זכה קוק בפרס טיורינג.

עד היום, לא נמצא אף אלגוריתם פולינומי לאף אחת מהשפות הנ"ל, והשאלה האם P=NP נותרה אחת השאלות הפתוחות העמוקות במדעי המחשב.

== הוכחת המשפט ==

להוכחה יש שני חלקים:
# SAT (כשפה הפורמלית הכוללת את כל הנוסחאות הספיקות) שייכת ל-NP; 
# יש רדוקציה פולינומית מכל בעיית NP ל-SAT.

=== בעיית הספיקות היא ב-NP ===
כדי להוכיח כי <math>SAT \in NP</math>, עלינו לתאר מכונת טיורינג אי דטרמיניסטית המכריעה את <math>SAT</math> בזמן פולינומי באורך הקלט. תהי <math>N_{SAT}</math> מכונת טיורינג אי דטרמיניסטית המקבלת קלט <math>\varphi(x_1, ..., x_n)</math>, אזי:
# נחש השמה <math>\pi</math> עבור המשתנים <math>x_1, ..., x_n</math>.
# לכל פסוקית <math>\varphi_i \in \varphi</math>:
## בדוק אם ההשמה <math>\pi</math> עבור המשתנים שנמצאים בפסוקית אכן מספקים אותה.
## אם לא, החזר "<math>\varphi</math> לא ספיקה".
# החזר "<math>\varphi</math> ספיקה".

==== הוכחת נכונות המכונה ====
<math display="block">\varphi \in SAT \implies \text{There is a satisfiable assignment for } \varphi \implies N_{SAT} \text{ will be able to guess this assignment, as there is an accpting path} \implies \varphi \in L(N_{SAT})</math>

<math display="block">\varphi \notin SAT \implies \varphi \text{ is unsatisfiable} \implies N_{SAT} \text{ will reject any guessed assignment} \implies \varphi \notin L(N_{SAT})</math>

==== ניתוח סיבוכיות זמן ריצה ====
בהינתן קלט <math>\varphi</math> עם <math>n</math> משתנים ו-<math>m</math> פסוקיות:
* שלב 1 ייקח זמן ריצה של <math>O(n)</math> שכן המכונה מנחשת השמה <math>T</math> או <math>F</math> לכל ה-<math>n</math> משתנים.
* שלב 2 ייקח זמן ריצה של <math>O(m \times n)</math> לכל היותר, שכן יש לנו <math>m</math> פסוקיות ו-<math>2n</math> ליטרלים לכל היותר בכל פסוקית.

לכן זמן ריצת המכונה הוא לכל היותר <math>O(m \times n)</math>, שזהו זמן ריצה פולינומי בגודל הקלט.

מסקנה: <math>SAT \in NP</math>

=== בעיית הספיקות היא NP-קשה ===

==קישורים חיצוניים==

* [http://www.cs.toronto.edu/~sacook/ אתר הבית של סטיבן קוק]
*

קטגוריה:בעיות NP-שלמות
קוק-לוין