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

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

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

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

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

משפט קוק מנסח NP-שלמות כך: בעיה היא NP-שלמה אם היא (1) שייכת ל-NP, ו-(2) כל בעיה ב-NP ניתנת להמרה אליה בזמן פולינומי. המרה פולינומית היא דרך יעילה להמיר מופע של בעיה אחרת למופע של הבעיה הנבדקת, מבלי לשנות את התשובה כן/לא.

המשמעות: אם יש אלגוריתם פולינומי ל-SAT, אז P=NP וניתן לפתור כל בעיה ב-NP במהירות.

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

ההוכחה כוללת שני חלקים קצרים:

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

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

התוצאה המשמעותית היא שאם נמצא אלגוריתם יעיל ל-SAT, נפתרת גם שאלת P=NP לטובת שוויון.

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

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

משפט קוק-לוין אומר שבעיה בשם SAT היא אחת הקשות בקבוצה שנקראת NP.

P הן בעיות שאפשר לפתור מהר. NP הן בעיות שאם נותנים פתרון, אפשר לבדוק מהר אם הוא נכון.

שאלה גדולה היא האם כל בעיה שאפשר לבדוק מהר אפשר גם לפתור מהר. זוהי שאלה פתוחה.

SAT היא בעיה של נוסחאות לוגיות. נוסחאות אלה כתובות עם משתנים שאפשר לשים להם אמת או שקר. שואלים אם יש דרך לתת ערכים למשתנים כך שהנוסחה תהיה אמת. צורת CNF היא צורה מסודרת של נוסחאות שמקלה על העבודה.

ההוכחה עושה שני דברים:
1) מראים שאם נותנים השמה (בחירה של אמת/שקר), אפשר לבדוק מהר אם היא מספקת את הנוסחה.
2) מראים שאפשר לקחת כל בעיה ב-NP ולהפוך אותה לבעיה של SAT כך שהתשובה לא משתנה.

אם ימצאו דרך לפתור את SAT מהר, אפשר לפתור הרבה בעיות אחרות מהר גם כן.

המשפט עזר להראות שבעיות רבות הן קשות באותה מידה. קוק ועמיתיו הראו את זה בשנות ה-70. עד היום לא נמצא פתרון מהיר ל-SAT.