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

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

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

השפה SAT היא דוגמה אחת לשפה שכזו, מאוד מעניינת: המחרוזות ששייכות אליה מקודדות פסוקים מתחשיב הפסוקים, שהם מהצורה הנורמלית CNF. כלומר, כל פסוק הוא מהצורה \( \varphi=C_{1}\wedge C_{2}\wedge\dots\wedge C_{n} \) כך שכל \( C_{i} \) כזו נקראת פסוקית והיא מהצורה \( C=\left(l_{1}\vee l_{2}\vee\dots\vee l_{k}\right) \) כאשר כל \( l_{j} \) כזה נקרא ליטרל והוא או משתנה או שלילה של משתנה (או מהצורה \( x \) או מהצורה \( \neg x \) עבור משתנה \( x \) כלשהו). שימו לב שמספר הליטרלים בכל פסוקית יכול להיות שונה; פסוק CNF פשוט לדוגמה הוא \( \left(x\vee\neg y\right)\wedge\left(\neg x\vee y\vee z\right) \).

פסוק CNF נקרא ספיק אם קיימת השמה של ערכי אמת למשתנים שלו שמספקת אותו. כדי לספק פסוק CNF צריך לספק בו זמנית את כל הפסוקיות שלו; כדי לספק פסוקית צריך לספק לפחות ליטרל אחד. כדי לספק משתנה צריך להציב בו את הערך True, וכדי לספק שלילה של משתנה צריך להציב באותו משתנה את הערך False. זה הכל. בפועל אני מייצג את True ו-False בעזרת 1 ו-0, בהתאמה.

הבעיה של הכרעה האם פסוק CNF כלשהו שייך ל-SAT היא בעיה קשה, מבחינה חישובית: אם יש לפסוק \( n \) משתנים בסך הכל (פזורים לכל רוחב הפסוקיות שלו, לפעמים עם שלילה) אז יש \( 2^{n} \) השמות אפשריות לפסוק, ולעבור אחת אחת ולבדוק את כולן - זה פתרון שהוא לא יעיל מבחינה חישובית. זה לא אומר שאין שיטות מתוחכמות יותר, אבל אין שיטה שמבטיחה תמיד, גם במקרה הגרוע ביותר, זמן ריצה שנחשב “יעיל” (פולינומי). עם זאת, ל-SAT יש גם תכונה נחמדה מאוד: אם נתון לכם פסוק \( \varphi \) שאכן שייך ל-SAT, אז אפשר לשכנע אתכם יחסית בקלות בכך אם נותנים לכם הוכחה מתאימה לכך - במקרה הזה, ה”הוכחה” היא פשוט השמה מספקת עבור הפסוק; אתם בודקים בעצמכם שההשמה אכן מספקת ולא מרמים אתכם, ואם היא מספקת, השתכנעתם שהפסוק שייך ל-SAT.

הרעיון הזה, של שפות שקל לבדוק הוכחה לשייכות של מילה אליהן מגדיר את המחלקה NP. פורמלית, \( L\in\mbox{NP} \) אם קיים מוודא שהוא מכונת טיורינג פולינומית (אחזור על הפורמליזם שמגדיר מכונות טיורינג בהמשך, כשאזדקק לכך) \( M \) כך ש-\( M \) רצה על זוג קלטים, \( x,y \); הרעיון הוא ש-\( x \) הוא המילה שאת שייכותה ל-\( L \) בודקים, ו-\( y \) הוא “הצעת הוכחה” לשייכות הזו. זמן הריצה הפולינומי של \( M \) נמדד רק ביחס ל-\( x \), או לחילופים דורשים שהגודל של \( y \) יהיה פולינומי בגודל של \( x \), אחרת במקום “הוכחה” היינו יכולים פשוט לדחוף \( y \) ג’יברישי ארוך מאוד ובכך לאפשר ל-\( M \) לרוץ המון זמן ולבדוק את שייכות \( x \) לשפה באופן ישיר, מה שכמובן מפספס את הפואנטה. עכשיו, אם \( x\in L \) הדרישה שלנו היא שקיים \( y \) כך ש-\( M \) מסיימת את ריצתה על הזוג \( x,y \) ואומרת “כן”, ואילו אם \( x\notin L \) אז לכל \( y \), \( M \) תסיים את ריצתה על \( x,y \) עם אמירת “לא”. שימו לב לחוסר הסימטריה פה (“קיים” אל מול “לכל”). זו כל ההגדרה. יש הגדרה שקולה, שמדברת על מכונת טיורינג אי דטרמיניסטית (וגם את ההגדרה שלי אפשר לנסח בצורה שונה, בעזרת יחסים) אבל אני לא אכנס לזה כרגע - ההוכחה שלי תהיה עבור ההגדרה שנתתי, והוכחות אחרות הן אותו הדבר בערך.

שפות ב-NP יש המון. המון המון המון. עשרות אלפי בעיות מעניינות במדעי המחשב הן בעלות התכונה היפה של NP. ולכן היה מעניין, במידת מה, לגלות שיש שפה ב-NP שמסוגלת לקודד את כולן. השפה הזו הייתה SAT, וזה התוכן של משפט קוק-לוין. למה אני מתכוון ב”לקודד”? בואו ניקח שפה \( L\in\mbox{NP} \) כלשהי; הטענה היא שלכל \( x \) (בין אם הוא ב-\( L \) ובין אם לאו) ניתן לבנות בזמן יעיל (פולינומי) פסוק CNF \( \varphi_{x} \) כך ש-\( \varphi_{x}\in\mbox{SAT} \) אם ורק אם \( x\in L \). לבניה כזו קוראים רדוקציה פולינומית. לכן, ניסוח אחר למשפט קוק-לוין הוא: SAT היא בעלת התכונה שכל שפה ב-NP ניתנת לרדוקציה פולינומית אליה. שפה עם תכונה שכזו נקראת NP-קשה; השם “NP-שלמה” בא להעיד על כך שזו שפה שהיא גם NP-קשה וגם שייכת בעצמה ל-NP.

את המשפט פרסם סטיבן קוק בארה”ב ב-1971. ב-1973 התפרסמה בבריה”מ גרסה אחרת של המשפט שהוכיח לאוניד לוין. זו הייתה אחת מתופעות הלוואי העגומות של המלחמה הקרה - תורת הסיבוכיות התפתחה בארה”ב ובברה”מ באופן בלתי תלוי, וגם הזמנים המדויקים לא ברורים לי (לוין כנראה הוכיח את המשפט הרבה לפני 1973). הניסוח של לוין היה שונה ומה שאני מציג הוא את הניסוח של קוק; אבל מה שלוין עשה עדיין תפס את לב העניין ולכן אני מעדיף לקרוא למשפט על שם שניהם.

משפט קוק היה אמנם מעניין, אבל על פניו הוא לא הוכיח משהו מרגש במיוחד - ניתן ללא קושי מהותי לייצר שפה מלאכותית שהיא NP-שלמה. אבל זה לב העניין - זו תהיה שפה מלאכותית ולא מעניינת, וההוכחה תהיה פשוטה בהתאם. לעומת זאת, קוק תפס שפה חשובה ושימושית, אבל לאף אחד כנראה לא היה ברור עד כמה היא שימושית עד שריצ’ארד קארפ בא בשנת 1972 והציג רשימה של 21 בעיות ב-NP - בעיות מרכזיות ומעניינות במדעי המחשב - ש-SAT ניתנת לרדקוציה אליהן בדרך זו או אחרת. עכשיו, די קל לראות שניתן להרכיב רדוקציות; לכן אם \( L_{1} \) ניתנת לרדוקציה אל SAT, ואילו SAT ניתנת לרדוקציה אל \( L_{2} \), אז \( L_{1} \) ניתנת לרדוקציה אל \( L_{2} \). המשמעות: קארפ הוכיח שעוד 21 בעיות הן NP-שלמות (יום אחד אני ארצה לתאר את כל המאמר שלו בבלוג - זו יצירת מופת של רדוקציות יצירתיות ופשוטות). מכאן כבר הזרם היה בלתי ניתן לעצירה. כדי להוכיח שבעיה היא NP-שלמה, כל מה שצריך לעשות הוא לרדקץ אליה בעיה אחרת, שאנחנו כבר יודעים שהיא NP-שלמה, וככל שאנחנו מכירים יותר כאלו, כך יהיה לנו קל יותר לרדקץ; כיום יש אלפי בעיות שאנו יודעים שהן NP-שלמות. וכל זה נובע מהבסיס, שהוא SAT, דהיינו משפט קוק-לוין.

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

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

הרעיון האינטואיטיבי הוא זה: נתונה לנו שפה \( L\in\mbox{NP} \). ניקח מכונת טיורינג \( M \) עבורה. כעת, בהינתן \( x \) כלשהו, נבנה פסוק \( \varphi_{x}\left(y\right) \) שבצורה מחוכמת כלשהי יקודד בתוכו חישוב של \( M \) על \( x,y \). שימו לב: כאן \( y \) מייצגים את המשתנים של הפסוק; הרעיון הוא שאנחנו יכולים להזין לפסוק ערכים שונים של \( y \), ושהפסוק יסתפק או לא יסתפק בהתאם לשאלה האם \( M \) מחזירה “כן” על \( x,y \) או “לא”. אבל זה רק הרעיון האינטואיטיבי. הביצוע יהיה קצת יותר מסובך. בפועל לקודד חישובים עם CNF זה לא טריוויאלי, אז אנחנו נשתמש גם במשתני עזר שאסמן \( z \), והפסוק יסומן \( \varphi_{x}\left(y,z\right) \). שימו לב - גם \( y \) וגם \( z \) מייצגים וקטורים של משתנים, לא משתנים בודדים; כלומר, אני משתמש בכתיב הזה בתור קיצור לכתיב \( \varphi_{x}\left(y_{1},\dots,y_{n},z_{1},\dots,z_{k}\right) \) שתסכימו איתי שהוא מסורבל יותר. הרעיון הוא שלמשתני העזר הללו לא יהיה חופש בחירה: בהינתן השמה כלשהי ל-\( y \)-ים, תהיה בדיוק דרך אחת שבה אפשר לתת ערכים ל-\( z \)-ים אם אנחנו מקווים להצליח לספק את הפסוק; כל דרך אחרת שבה נציב ערכים ב-\( z \)-ים אוטומטית תגרום לכך שהפסוק לא יסתפק על ידי ההשמה הזו.

כדי להבין איך נראה חישוב של \( M \) צריך להיזכר בפרטים הטכניים של איך נראית מכונת טיורינג. יש למכונה סרט אינסופי שמחולק לתאים, כשבכל תא יכול להיות סימבול מתוך קבוצת סימבולים שנקראית אלפבית הסרט, \( \Gamma \). בנוסף יש למכונה ראש קורא וכותב שבכל רגע נתון נמצא מעל תא אחד בסרט, ומחובר למערכת בקרה שיכולה להימצא במצבים פנימיים שונים ומשונים מתוך קבוצה סופית \( Q \) של מצבים. כל רגע נתון בחישוב ניתן לתיאור מלא באמצעות שלושה פרטים: המצב הפנימי הנוכחי של המכונה; המיקום של הראש; התוכן הנוכחי של הסרט. שלשה כזו נקראת קונפיגורציה וחישוב של מכונת טיורינג הוא סדרה של קונפיגורציות, שכל אחת מתקבלת מקודמתה בהתאם לפונקצית המעברים של המכונה; זו פונקציה \( \delta:Q\times\Gamma\to Q\times\Gamma\times\left\{ L,R,S\right\} \) שלכל זוג \( \left(q,\sigma\right) \) של “המצב הפנימי הנוכחי \( q \) והתו \( \sigma \) שהראש כרגע קורא” מתאימה שלשה \( \left(p,\tau,X\right) \) שמשמעותה “עבור למצב \( p \); כתוב \( \tau \) על הסרט במקום \( \sigma \); והזז את הראש בהתאם ל-\( X \) (כאשר ימינה זה \( R \), שמאלה זה \( L \) והישארות במקום זה \( S \))”.

מכונה יכולה להיכנס למצב פנימי מיוחד שמסומן ב-\( q_{acc} \) שמשמעותו שהיא עצרה ואמרה “כן”; באופן דומה המצב \( q_{no} \) אומר שהמכונה עצרה ואמרה “לא”. קונפיגורציה שבה זה המצב הפנימי של המכונה נקראת קונפיגורציה סופית. פרט לכך יש גם קונפיגורציה התחלתית מוסכמת - זו שבה כל הסרט ריק פרט לקלט של המכונה (במקרה שלנו, הזוג \( x,y \)), הראש הקורא נמצא בקצה השמאלי של הסרט (הקצה הימני לא קיים; זו המשמעות של האינסופית של הסרט) והמצב הפנימי של המכונה הוא איבר מיוחד של \( Q \) שמסומן לרוב ב-\( q_{0} \).

אז השאלה שלנו היא זו: האם קיימת למכונה סדרת קונפיגורציות חוקיות כך שהקונפיגורציה ההתחלתית מתאימה לקלט \( x,y \), והסדרה מסתיימת בקונפיגורציה סופית מקבלת? המשתנים \( z \) שלנו הולכים לקודד את סדרת הקונפיגורציות הזו.

עכשיו, לכאורה יש לנו בעיה כאן - איך נייצג קונפיגורציה, שהרי היא אינסופית? וכמו כן, גם סדרת הקונפיגורציות עשויה להיות באורך לא חסום. כאן נחלצת לעזרתנו העובדה ש-\( M \) היא פולינומית. זה אומר שקיים פולינום \( p\left(n\right) \) כך שמספר הצעדים המקסימלי ש-\( M \) מבצעת על \( x,y \) הוא \( p\left(\left|x\right|\right) \). זה אומר שמספיק לנו להסתכל על \( p\left(\left|x\right|\right)+1 \) התאים הראשונים של הסרט, כי \( M \) לא תגיע רחוק יותר, ועל סדרת קונפיגורציות מאורך \( p\left(\left|x\right|\right)+1 \) כי \( M \) לא תבצע חישוב ארוך יותר. בואו נסמן \( m=p\left(\left|x\right|\right)+1 \) אם כך.

כדי לעשות לעצמי את החיים קלים יותר, אני הולך להניח כמה הנחות מקלות על \( M \). ראשית, שהיא מבצעת בדיוק \( p\left(\left|x\right|\right) \) צעדים, בלי תלות בערך של \( y \), ובצעד האחרון עוברת לקונפיגורציה סופית. זה יחסוך לי את הטורח של לבדוק האם המכונה נעצרה בקונפיגורציה מוקדמת יותר מהאחרונה (זה לא טורח גדול, ועדיין). למה אפשר להניח את זה? כי קל לקחת את \( M \) שנתונה לי ולשנות קצת את הקידוד שלה כך שאם היא התכוונה להיכנס למצב סופי, היא “תתאפק קצת” ותחכה. לשם כך היא צריכה לתחזק מונה שסופר את הצעדים שלה וכדומה, אבל אפשר לעשות דברים כאלו עם מכונות טיורינג. זה מגדיל קצת את זמן הריצה - משנה את הפולינום \( p \) - אבל זמן הריצה עדיין יהיה פולינומי. באופן דומה, אני אניח שה-\( y \)-ים שהמכונה יכולה לקבל יחד עם \( x \) לא ארוכים מדי הם כולם מאותו האורך (אם זה מטריד אתכם תחשבו על כך שהמכונה יכולה לרוץ על כל הרישות של ה-\( y \) שקיבלה) וש-\( p \) גדול דיו כך שיש מקום ל-\( x,y \) על \( m \) התאים הראשונים של הסרט (על פניו הרשיתי ל-\( y \) להיות ארוך יותר, אבל אם המכונה לא תספיק לקרוא את כל התאים של \( y \) אפשר להחליף אותו ברישא של עצמו).

האינטואיציה עכשיו היא שלכל \( 1\le i,j\le m \) יהיה לנו משתנה \( z_{i,j} \) שאומר מה נמצא בתא ה-\( j \) בסרט בקונפיגורציה ה-\( i \)-ית; חשבו על זה בתור טבלה גדולה שבה השורות הן הקונפיגורציות, והעמודות הן התאים האינדיבידואליים בסרט. אני ארצה לכתוב דברים כמו \( z_{i,j}=\sigma \) כדי לומר שיש את האות \( \sigma \) בתא הזה. והנה מגיע טריק נחמד: אני יכול “לדחוף פנימה” גם את שני הפרמטרים הנוספים של הקונפיגורציה - המיקום של הראש והמצב הפנימי של המכונה. אם, למשל, בקונפיגורציה \( i \) הראש מצביע על התא \( j \), המצב הפנימי הוא \( q \) ותוכן התא הזה הוא \( \sigma \), אז במקום \( z_{i,j}=\sigma \) המשתנה יגיד \( z_{i,j}=\left(q,\sigma\right) \). כלומר, הטבלה בגודל \( m\times m \) שלי מקודדת את כל המידע הדרוש על הקונפיגורציות.

אבל הנה בעיה: המשתנים שיש לי בפסוק CNF לא יכולים לקודד סימבולים מסובכים. הם בסך הכל יכולים לקבל ערכים של T ו-F. אלו משתנים בוליאניים. אז מה עושים? הפתרון לא מסובך במיוחד וסטנדרטי עבור מי שרגיל לקודד דברים עם CNF-ים; חלק מהקושי בהוכחה של משפט קוק-לוין ללא ספק נובע מכך שרוב מי שרואים אותו לא רגילים עדיין לשום דבר מסוג זה.

פתרון אחד הוא להתייאש ולתהות למה קוק טרח מלכתחילה להתעסק עם SAT ולא עם שפה גמישה קצת יותר. זו תשובה לגיטימית ויש ספרי לימוד שאכן משתמשים בוריאציה יותר מתוחכמת על השפה לצורך המשפט. אבל אני חושב שכדאי להישאר עם SAT כי זה לא כזה נורא. הרעיון הוא כזה: עבור כל ערך אפשרי \( \gamma \) שעשוי להתקבל על ידי המשתנה \( z_{i,j} \) שלנו (כלומר, תו \( \sigma \) או ביטוי מסובך יותר כמו \( \left(q,\sigma\right) \)) יהיה לנו משתנה בוליאני \( z_{i,j}^{\gamma} \). הרעיון הוא איכשהו להבטיח שלכל \( i,j \), בדיוק אחד מבין המשתנים \( z_{i,j}^{\gamma} \) יקבל את הערך T, והמשמעות של זה תהיה \( z_{i,j}=\gamma \).

כדי להבטיח שלפחות אחד מבין המשתנים יקבל T, אנחנו מוסיפים לפסוק שאנו בונים את הפסוקית \( \bigvee_{\gamma}z_{i,j}^{\gamma} \), כלומר הפסוקית תכיל את כל המשתנים מהצורה \( z_{i,j}^{\gamma} \) עבור \( i,j \) קבוע וכל ה-\( \gamma \) האפשריים.

כדי להבטיח שלכל היותר אחד מבין המשתנים יקבל T, אני מוסיף הרבה פסוקיות מהצורה \( \neg z_{i,j}^{\gamma}\vee\neg z_{i,j}^{\gamma^{\prime}} \), לכל זוג \( \gamma\ne\gamma^{\prime} \) של ערכים אפשריים. פסוקית כזו אומרת “או ש-\( z_{i,j}\ne\gamma \) או ש-\( z_{i,j}\ne\gamma^{\prime} \)”, כלומר, באופן שקול, “לא ייתכן שגם \( z_{i,j}=\gamma \) וגם \( z_{i,j}=\gamma^{\prime} \)”.

יפה. אז מעכשיו אני יכול להשתמש בחופשיות בסימון \( z_{i,j}=\gamma \) כשבעצם ברור שהכוונה היא למשתנה \( z_{i,j}^{\gamma} \). מה שהשגתי עד כה הוא שבניתי פסוק שכל השמה שמספקת אותו מגדירה סדרה של \( m \) קונפיגורציות מאורך \( m \). מה נשאר לי לעשות? את הדברים הבאים:

1. להבטיח שהקונפיגורציה הראשונה בסדרה היא הקונפיגורציה ההתחלתית של \( M \) על \( x,y \).
2. להבטיח שהקונפיגורציה האחרונה בסדרה היא מקבלת.
3. להבטיח שהמעבר בין כל שתי קונפיגורציות סמוכות הוא חוקי.

את \( 1 \) קל להבטיח. נסמן \( x=x_{1}\cdots x_{k} \) ו-\( y=y_{1}\cdots y_{n} \), ונוסיף לפסוק שלנו פסוקיות שאומרות \( z_{1,1}=\left(q_{0},x_{1}\right) \) (כן, יש כאן מקרה קצה אם \( x \) ריק; אני בטוח שתדעו להתמודד איתו בעצמכם) ו-\( z_{1,i}=x_{i} \) עבור \( i>1 \) ו-\( z_{1,k+1}=, \) (שווה לסימן פסיק, או מה שזה לא יהיה שנשתמש בו בתור מפריד בין \( x \) ו-\( y \)) ו-\( z_{1,k+1+i}=y_{i} \). האחרון מעניין, כי ה-\( y_{i} \)-ים הם לא קבועים - הם בעצמם משתנים. איך מקודדים את זה? ובכן, אם תזכרו שניה מה הקיצורים שלי מסמנים, אני בעצם מוסיף את הפסוקיות שמקודדות את הטענות הבאות: \( z_{1,k+1+i}^{1}=y_{i} \) ו-\( z_{1,k+1+i}^{0}=\neg y_{i} \) (שימו לב שמספיק לטפל בערכים 0 ו-1 כי זה כל מה ש-\( y \) יודע לקבל). אז יש לנו כאן שאלה כללית יותר של קידוד CNF-ים - איך מקודדים \( x=y \)? בקלות, הפסוקיות \( \left(x\vee\neg y\right)\wedge\left(\neg x\vee y\right) \). ואיך מקודדים \( x=\neg y \)? בקלות, וזה נובע ממה שכבר ראינו: \( \left(x\vee y\right)\wedge\left(\neg x\vee\neg y\right) \).

את 2 גם כן קל להבטיח על ידי פסוקית ענק שבודקת אם במקרה יש לנו מצב מקבל בקונפיגורציה האחרונה: \( \bigvee_{i,\sigma}z_{m,i}=\left(q_{acc},\sigma\right) \) כאשר כאן אנחנו רצים גם על כל \( 1\le i\le m \) וגם על כל \( \sigma \) אפשרי. יכלנו להניח עוד הנחות על המכונה כדי לפשט את החיים (למשל, שהיא חוזרת לתא הראשון בסרט ומרוקנת אותו לפני שהיא עוברת למצב מקבל) אבל הנוסחה פשוטה מספיק גם ככה לטעמי.

נשאר לנו רק 3, שהוא לב העניין. שימו לב שעד עכשיו הפסוק שבנינו היה פולינומי בגודלו - הוספנו רק מספר פולינומי של פסוקיות מגודל פולינומי (פולינומי בגודל של \( x \)). האתגר מגיע כשאנחנו רוצים להבטיח שכל שתי קונפיגורציות סמוכות מייצגות מעבר חוקי. על פניו יש המוני אפשרויות לזוגות כאלו ולכו תבדקו אותם ומהומה והצילו ולא מובטח על פניו שנקבל פסוק פולינומי שמקודד את כל המהומה הזו. לב לבו של העניין ושל כל המשפט נעוץ בכך שמכונת טיורינג היא מודל חישובי שמבצע שינויים לוקליים - בכל צעד חישוב, השינוי שעובר על תא אחד בקונפיגורציה לא מושפע מכל הקונפיגורציה הקודמת, אלא רק מכמה תאים בקונפיגורציה הקודמת. זה אומר שאם אני רוצה לכתוב את הערך של \( z_{i+1,t} \), אני צריך לכתוב פסוקיות שמחשבות כפונקציה של מספר מצומצם של משתנים \( z_{i,r} \). אם לחדד, כל תא יכול להיות מושפע רק מהתא שבשורה הקודמת ומשני שכניו של התא הזה. הנה דוגמה שתמחיש את זה.

נניח שאני תא מס’ 8 בשורה 5 ואני רוצה לדעת מה אמור להיות הערך שלי, על פי מה שקורה בשורה 4. הנה התרחישים שאני צריך להתחשב בהם:

1. הראש של המכונה היה בתא 8 בשורה 4. במקרה הזה, לא משנה מה הראש מחליט לעשות, תא 8 בשורה 5 יהיה פונקציה בלעדית של תא 8 בשורה 4.
2. הראש של המכונה היה בתא 7 בשורה 4. במקרה הזה, ייתכן שהראש יחליט לפנות ימינה (להגדיל את מס' התא שלו ב-1) ואז תא 8 יפסיק להכיל \( \sigma \) ויעבור להכיל \( \left(q,\sigma\right) \) עבור \( q \) כלשהו.
3. הראש של המכונה היה בתא 9 בשורה 4. במקרה הזה, ייתכן שהראש יחליט לפנות שמאלה וזה כמו במקרה הקודם.
4. כל מיקום אחר של הראש גורר שהוא לא יוכל להשפיע בשום צורה על תא 8.

אם כן, לכל \( \gamma \), הערך של המשתנה \( z_{i,j}^{\gamma} \) נקבע לכל היותר על ידי המשתנים \( z_{i-1,j-1}^{\gamma^{\prime}} \), \( z_{i-1,j}^{\gamma^{\prime}} \) ו-\( z_{i-1,j+1}^{\gamma^{\prime}} \) עבור כל \( \gamma^{\prime} \) אפשרי. זו קבוצה לא קטנה של משתנים, אבל גם לא גדולה יותר מדי. יש בה שלושה איברים כפול מספר ה-\( \gamma^{\prime} \) האפשריים. כזכור, \( \gamma \) הוא או תו מאלפבית הסרט \( \Gamma \) או שהוא זוג של תו מאלפבית הסרט ומצב פנימי \( Q \) של המכונה. אז יש לנו בסך הכל \( \left|\Gamma\right|+\left|\Gamma\right|\left|Q\right| \) אפשרויות כאלו. לכן כל משתנה תלוי לכל היותר ב-\( 3\left(\left|\Gamma\right|+\left|\Gamma\right|\left|Q\right|\right) \) משתנים אחרים. עכשיו מגיע נפנוף הידיים היחיד שאני מרשה לעצמי בהוכחה, כי הוא ברור לכל מי שמכיר קצת CNF-ים: כל קשר מהצורה \( a=f\left(b_{1},b_{2},\dots,b_{n}\right) \) כאשר \( f \) היא פונקציה בולינאנית אפשר לתאר באמצעות CNF, במובן זה שלכל הצבה אפשרית של ערכים ל-\( b_{1},\dots,b_{n} \), הפסוק מסתפק אם ורק אם מציבים ב-\( a \) את \( f\left(b_{1},\dots,b_{n}\right) \). מה שעשיתי קודם, עם \( x=y \) היה מקרה פרטי פשוט של זה.

בכל זאת, אם אתם סקרנים, הנה הרעיון הכללי. \( a=f\left(b_{1},b_{2},\dots,b_{n}\right) \) זו פשוט דרך אחרת לכתוב פונקציה כללית יותר, \( g\left(a,b_{1},\dots,b_{n}\right) \), שמקבלת 1 כאשר \( a=f\left(b_{1},b_{2},\dots,b_{n}\right) \) ו-\( 0 \) אחרת. אז האתגר שלנו הוא רק לדעת איך כותבים CNF עבור פונקציה בוליאנית כללית. לצורך כך קל יותר לחשוב על איך כותבים DNF, שהוא המושג הדואלי ל-CNF: זה פסוק מהצורה \( C_{1}\vee\dots\vee C_{n} \) כאשר כל פסוקית היא מהצורה \( \left(l_{1}\wedge\dots\wedge l_{k}\right) \). פסוק כזה מקבל 1 אם ורק אם לפחות אחת מהפסוקיות מסתפקת; הרעיון הוא שכל פסוקית תתאים לשורה בטבלת האמת של \( g \). תוכן הפסוקית יתאים לערכים שהמשתנים של \( g \) מקבלים באותה שורה. למשל, אם \( g\left(x,y,z\right) \) היא פונקציה כך ש-\( g\left(1,0,1\right)=1 \) אז הפסוקית שתתאים להשמה הזו תהיה \( x\wedge\neg y\wedge z \).

כעת, קל לראות שאם \( \varphi \) הוא פסוק DNF אז \( \neg\varphi \) הוא בעצם פסוק CNF בתחפושת - רק צריך להשתמש בכללי דה-מורגן כדי לדחוף את ה-\( \neg \) פנימה. למשל, בואו נכתוב DNF עבור \( x=y \): בבירור זה ה-DNF \( \left(x\wedge y\right)\vee\left(\neg x\wedge\neg y\right) \). עכשיו נפעיל \( \neg \) על הכל ונקבל:

\( \neg\left[\left(x\wedge y\right)\vee\left(\neg x\wedge\neg y\right)\right]\equiv\neg\left(x\wedge y\right)\wedge\neg\left(\neg x\wedge\neg y\right)\equiv\left(\neg x\vee\neg y\right)\wedge\left(\neg\neg x\vee\neg\neg y\right)\equiv\left(\neg x\vee\neg y\right)\wedge\left(x\vee y\right) \)

וקיבלנו CNF עבור השלילה של \( x=y \), כלומר עבור \( x\ne y \). המסקנה: אם אני רוצה למצוא CNF עבור \( g \), בואו נמצא DNF עבור \( \neg g \) ואז נפעיל עליו \( \neg \).

כמובן, נשאלת השאלה מה גודל ה-CNF הזה. התשובה היא שהוא עשוי להיות ענקי. אקספוננציאלי במספר המשתנים של \( g \). כך גם אצלנו - הגודל של הפסוקיות שאני מוסיף עבור כל תא \( z_{i,j} \) שאני רוצה לתאר את הפונקציה שלו עשוי להיות אקספוננציאלי. אבל אקספוננציאלי במה? במספר שחישבתי קודם, \( 3\left(\left|\Gamma\right|+\left|\Gamma\right|\left|Q\right|\right) \). המספר הזה אינו תלוי בגודל הקלט \( x \) שאנחנו עושים עבורו את הרדוקציה; זה קבוע שמתאר את המורכבות של המכונה עבור \( L \) ותו לא.

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

האם סיימנו את ההוכחה? באופן מפתיע למדי, כן! קיבלנו פסוק \( \varphi_{x}\left(y,z\right) \) כך שלכל הצבה של ערכים ל-\( y \), מתקיים אחד משניים: אם \( M \) מקבלת את \( x,y \), אז קיימת הצבה (יחידה) של ערכים ל-\( z \) שמספקת את \( \varphi_{x}\left(y,z\right) \); ואם \( M \) דוחה את \( x,y \) אז כל הצבה של ערכים ל-\( z \)-ים לא תספק את \( \varphi_{x} \). כלומר, \( \varphi_{x} \) הוא ספיק אם ורק אם \( x\in L \). יותר מכך - יוצא שמספר ההשמות המספקות של \( \varphi_{x} \) שווה למספר ה-\( y \)-ים שעבורם \( M \) מקבלת את \( x,y \) (מספר ה”הוכחות” השונות של \( x \)). השוויון הזה מעניין כי הוא מצביע על השימושיות האפשרית של משפט קוק-לוין גם בטענות מתוחכמות יותר מסתם “SAT היא NP-שלמה”, ואכן בנושאים מתקדמים יותר בסיבוכיות עושים וריאציות שכאלו על קוק-לוין כל הזמן; אבל אני אסתפק במה שהראיתי ואעצור כאן.