הצגת המקור של הדף "משפט קוק-לוין"

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

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

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

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

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

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

==תיאור פורמלי==
קוק הגדיר את המושג של בעיה [[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/ אתר הבית של סטיבן קוק]
*{{לא מדויק|1=2015/07/23/cook_levin_theorem/|2=משפט קוק-לוין}}

[[קטגוריה:בעיות NP-שלמות]]
[[קטגוריה:משפטים במדעי המחשב|קוק-לוין]]