משפט קוק-לוין
משפט קוק-לוין הוא משפט יסודי בתורת הסיבוכיות, הקובע שהבעיה 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 נותרה אחת השאלות הפתוחות העמוקות במדעי המחשב.
הוכחת המשפט
קישורים חיצוניים
- אתר הבית של סטיבן קוק
- גדי אלכסנדרוביץ', משפט קוק-לוין, באתר "לא מדויק", 23 ביולי 2015
35969077משפט קוק-לוין