NL=coNL ("משפט אימרמן") - מי, מה, כמה ולמה

בשעה טובה אנו עוברים לתיאור התוצאה השניה ב”תוצאות מפתיעות בסיבוכיות” - הטענה \( \mbox{NL=coNL} \), או בשמה הקליט יותר, משפט אימרמן-סזלפסני (Immerman–Szelepcsényi - אין לי מושג איך לתעתק נכון), ומכאן ואילך - משפט אימרמן. אז על מה מדובר בכלל?

ראשית כל תזכורת כללית למה אנחנו עושים בתורת הסיבוכיות. המטרה היא לסווג בעיות לפי כמות המשאבים הנדרשת כדי לפתור אותן (כמות שנמדדת תמיד ביחס לגודל הקלט שאיתו מנסים להתמודד). לצורך פשטות, אנחנו אוהבים להתעסק במיוחד בבעיות “כן/לא” - בעיות שבהן מביאים לנו קלט מסויים ושואלים אותנו האם הוא מקיים תכונה מסויימת (תכונה שהיא חלק מהגדרת הבעיה). למשל - נתון לנו גרף (מהו גרף? זה ידע קודם שנדרש למי שרוצה לקרוא פוסטים על מדעי המחשב) ושני צמתים בו - \( s,t \) - ואנו רוצים לדעת אם קיים בגרף מסלול מ-\( s \) אל \( t \). שימו לב לאופי ה”כן/לא”-י של הבעיה - לא ביקשנו לדעת מהו המסלול, אלא רק לדעת אם הוא קיים.

ייתכן שנראה לכם קצת מוזר שאפשר יהיה לגלות אם קיים מסלול בלי למצוא אותו במפורש, אבל יש בעיות שבהן זה קצת יותר ברור - למשל, בהינתן מספר \( n \), לגלות שהוא אינו ראשוני, כלומר קיים מספר בין 1 ל-\( n \) שמחלק אותו - את זה אפשר לבצע ביעילות, בעוד שלא ברור איך אפשר למצוא ביעילות מספר שמחלק את \( n \) (איך? יש כמה שיטות ותיארתי בעבר אחת מהן; אם מוצאים \( a \) כך שבמהלך החישוב של \( a^{n} \) מודולו \( n \) מתגלה שורש יחידה לא טריוויאלי - זה אומר מייד ש-\( n \) אינו ראשוני אף שזה כלל לא רומז על האופן שבו ניתן לפרק אותו).

כפי שמראה הדוגמה שלמעלה, בשאלות “כן/לא” רבות אפשר לתת תשובה חיובית בקלות אם נותנים לכם “רמז” לכך שהתשובה אכן חיובית. למשל, בשאלת הגרף - אם ייתנו לכם את מסלול בין \( s \) ו-\( t \), החיים יהיו קלים יותר - במקום לחפש מסלול בעצמכם רק תצטרכו לבדוק שהמסלול שנתנו לכם הוא בסדר. שימו לב שאם התשובה היא “לא”, לא ממש ברור איזה רמז אפשר לתת שישכנע אתכם בכך שהתשובה היא אכן שלילית.

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

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

בואו נעבור לקצת טרמינולוגיה מדוייקת. במקום לדבר כל הזמן על “בעיות”, מדעני מחשב מדברים על “שפות”. שפה \( L \) היא קבוצה של מילים - מחרוזות סופיות של תווים שמייצגות מידע כלשהו (יכול להיות קידוד של גרף, מספר, קוד של תוכנית מחשב וכדומה - תלוי בהקשר). למשל, אפשר לדבר על השפה שמכילה את כל השלשות \( \left(G,s,t\right) \) של גרף \( G \) עם צמתים \( s,t \) שיש מסלול ביניהם. השפה המשלימה ל-\( L \) מסומנת ב-\( \overline{L} \) - זו שפת כל המחרוזות שאינן ב-\( L \) (מראש אנחנו מניחים שמדובר רק על מחרוזות בינאריות, נאמר, כך שהשאלה מהי “קבוצת כל המחרוזות” שלוקחים משלים ביחס אליה איננה בעייתית). למשל, אם \( L \) היא שפת השלשות \( \left(G,s,t\right) \) שתיארתי קודם, אז \( \overline{L} \) היא שפת השלשות \( \left(G,s,t\right) \) של גרף \( G \) עם צמתים \( s,t \) שאין ביניהם מסלול. אולי תגידו עכשיו שיש גם הרבה מחרוזות שבכלל לא מייצגות שלשה \( \left(G,s,t\right) \) וגם הן אמורות להיות ב-\( \overline{L} \); כדי להיפרד מהמטרד הלא חשוב הזה נוח להניח שכל מחרוזת שמייצגת ג’יבריש תיחשב על ידינו ככזו שמייצגת איזה קלט טריוויאלי - למשל \( \left(G,s,t\right) \) כאשר \( G \) הוא גרף ששני הצמתים היחידים בו הם \( s,t \) ואין קשתות. הדברים הללו לא קריטייים ממילא ולא אחזור אליהם.

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

כעת אפשר להציג את \( \mbox{coNP} \): בפשטות, זו המחלקה של כל המשלימות של שפות ב-\( \mbox{NP} \): \( \mbox{coNP}=\left\{ \overline{L}|L\in\mbox{NP}\right\} \). כפי שתיארתי לעיל, זו מחלקת השפות שיש עבורן תהליך-בדיקת-עדים כך שעבור תשובת “לא” קיים \( y \) שמוכיח זאת, ועבור תשובת “כן” אין אף \( y \) שיעבוד עלינו ויגרום לנו לחשוב שהתשובה היא “לא”. וכעת לשאלת המחץ: האם \( \mbox{NP}=\mbox{coNP} \)?

האם העובדה שקל להוכיח שמשהו הוא “כן” גוררת שיהיה קל להוכיח אם הוא “לא”, ולהפך? האם העולם סימטרי ונחמד? זו השאלה. נתון גרף ונשאלת השאלה אם אפשר לצבוע אותו בשלושה צבעים. אם מישהו יתן לי את הצביעה יהיה לי קל לבדוק שהגרף אכן ניתן לצביעה כזו; האם יש דרך פשוטה במידה דומה לשכנע אותי שהגרף לא ניתן לשום צביעה? אםh תוכיחו את זה, הוכחתם כי \( \mbox{NP=coNP} \). אני מקווה שאתם מרגישים את חוסר הסימטריה המשווע שיש כאן; הוא הסיבה לכך שהאמונה הרווחת היא ש-\( \mbox{NP}\ne\mbox{coNP} \).

ייתכן שאתם תוהים מה הקשר של השאלה הזו לשאלה המפורסמת ביותר, האם \( \mbox{P=NP} \) (\( \mbox{P} \) היא מחלקת השפות שניתן להכריע עם אלגוריתם פולינומי שכלל לא נזקק לעדים). ובכן, אם \( \mbox{P=NP} \) אז \( \mbox{NP=coNP=P} \) (וזאת מכיוון ש-\( \mbox{P} \) סגורה למשלים), אבל אם \( \mbox{P}\ne\mbox{NP} \) (וכך סבורים כולם, כמעט) זה לא אומר ש-\( \mbox{NP}\ne\mbox{coNP} \). כך שזו שאלה “עדינה” יותר מאשר \( \mbox{P}\ne\mbox{NP} \) והוכחה עבורה תהיה קשה יותר מאשר הוכחה ש-\( \mbox{P}\ne\mbox{NP} \) (שכן הוכחה ש-\( \mbox{NP}\ne\mbox{coNP} \) תוכיח בפרט ש-\( \mbox{P}\ne\mbox{NP} \)).

עכשיו בואו ונבצע שינוי מחשבתי כלשהו. במקום לדבר על יעילות בצריכת משאב הזמן, נדבר על יעילות בצריכת משאב הזכרון. זמן ריצה נמדד במספר הצעדים שנדרשו לחישוב במודל הסטנדרטי של מכונת טיורינג - איך אפשר למדוד צריכת זכרון? הגישה הנאיבית מדברת על מודל של מכונת טיורינג עם סרט בודד שבו ראשית כל נכתב הקלט, ואחריו אפשר לכתוב עוד דברים לפי הצורך. אפשר להגדיר את כמות הזכרון שהמכונה צורכת בתור האינדקס של התא הקיצוני ביותר שאליו המכונה מגיעה במהלך החישוב (במילים אחרות - אם הזכרון היה סופי, מה כמות הזכרון המינימלית שלא הייתה גורמת לתוכנית להתרסק על הקלט הנתון). הבעיה עם הגישה הזו היא שאם התוכנית רוצה לקרוא את כל הקלט . (אפילו אם אינה רוצה לכתוב שום דבר) היא צריכה ללכת עד לקצה הקלט וזה כבר יניב שסיבוכיות הזכרון שלה היא לפחות \( \Omega\left(n\right) \). אלא שכאשר מדובר על סיבוכיות זכרון, סיבוכיות שנחשבת “יעילה” היא דווקא משהו מסדר גודל לוגריתמי ב-\( n \), ואת זה בשיטה שלנו אי אפשר למדוד בכלל. אז מה עושים?

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

כעת אפשר להכניס לתמונה סוף סוף את \( \mbox{NL} \)- זו מחלקת השפות שקיימת מכונה-בודקת-עדים עבורן שפועלת בסיבוכיות זכרון \( O\left(\log n\right) \). את \( \mbox{coNL} \) מגדירים באותו אופן כמו \( \mbox{coNP} \). לא מדויק עד הסוף לומר שאלו האנלוגים של \( \mbox{NP} \) ו-\( \mbox{coNP} \) כי גם סיבוכיות זכרון של \( O\left(\log^{k}n\right) \) (“פולי-לוגריתמית”) נחשבת יעילה; אבל שתי המחלקות הללו הן הבסיס. ולכן זו הפתעה לא קטנה כשמתברר שהאנלוג לשאלת \( \mbox{NP=coNP} \) עבור סיבוכיות זכרון זוכה לתשובה, ותשובה חיובית דווקא - \( \mbox{NL=coNL} \), ויותר מכך - לכל מחלקה דומה של סיבוכיות זכרון עבור חסם סיבוכיות גדול יותר, השוויון עדיין מתקיים (פורמלית, \( \mbox{NSPACE}\left(f\left(n\right)\right)=\mbox{coNSPACE}\left(f\left(n\right)\right) \) לכל \( f\left(n\right)\ge\log n \) שהיא מה שנקרא Space Constructible, כלומר ניתן לחשב את \( f\left(n\right) \) מתוך \( 1^{n} \) תוך שימוש ב-\( f\left(n\right) \) זכרון - זו דרישה טכנית שלא ניכנס כעת אליה). הטענה הוכחה בנפרד בידי אימרמן ובידי סזלפסני, ואין לי מושג מי מהם המציא את ההוכחה שאציג כעת (או אפילו אם מישהו מהם המציא אותה ולא שמדובר על המצאה מאוחרת יותר).

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

הסיבה לכך שהבעיה הזו כל כך חשובה היא שניתן לתאר חישובים של מכונות (ובפרט מכונות לבדיקת עדים) על קלט כלשהו באמצעות גרף - גרף הקונפיגורציות של המכונה, שכל צומת בו מתאר את המצב הנוכחי של המכונה - תוכן סרט הזכרון, מצב הבקרה הנוכחי, מיקום הראשים הקוראים בכל הסרטים - כל זה מידע שניתן לייצג בזכרון לוגריתמי, כך שניתן לשמור צומת בודד של הגרף בזכרון בכל עת. בגרף יש קשת מצומת א’ לצומת ב’ אם אפשר להגיע בצעד בודד מהקונפיגורציה א’ לקונפיגורציה ב’ (השאלה אם זה באמת קורא תלויה בשאלה מה רואים הראשים הקוראים בסרטי הקלט והעד). בפועל בהינתן הקידוד של צומת בגרף, אפשר לחשב בזכרון לוגריתמי את הצמתים שאליהם ניתן לעבור ממנו. לכן השאלה האם המכונה מקבלת קלט כלשהו מצטמצמת לשאלה אם קיים מסלול בגרף הקונפיגורציות שלה מהקונפיגורציה ההתחלתית לאיזו שהיא קונפיגורציה שבה המכונה עוצרת ומקבלת. אפשר להנדס את המכונה כך שתהיה רק קונפיגורציה אחת כזו (למשל, כזו שבה כל סרט העבודה מחוק והראשים הקוראים בתחילת כל הסרטים) ולכן אנחנו מצטמצמים לשאלה האם קיים מסלול בגרף בין שני צמתים - בדיוק בעיית הישיגות, \( \mbox{CON} \).

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

לבדוק שיש מסלול מ-\( s \) אל \( t \) בסיבוכיות זכרון יעילה, בהינתן עד לכך, את זה קל לעשות. העד יהיה תיאור המסלול עצמו, ולכן כל המידע שצריך לזכור בכל שלב הוא מה הצומת הנוכחי שלנו, לקרוא את הצומת הבא בתור מהעד, ולבדוק אם אכן יש קשת מהצומת הנוכחי שלנו אל הצומת הבא בתור שהעד מדבר עליו. מכיוון שלייצג צומת או שניים בודדים דורש רק כמות לוגריתמית של זכרון, זה מראה ש-\( \mbox{CON}\in\mbox{NL} \). האתגר הוא להראות ש-\( \mbox{CON}\in\mbox{coNL} \) - שיש עד לכך שלא קיים מסלול מ-\( s \) אל \( t \). איך עושים דבר כזה? התשובה פשוטה - אומרים את האמת, רק האמת, וכל האמת.

נניח שידוע לנו שיש בדיוק \( k \) צמתים שאליהם אפשר להגיע מ-\( s \) תוך לכל היותר \( n \) צעדים. אנחנו לא יודעים מיהם הצמתים הללו, אבל כוח משמיים הבטיח לנו כי יש בדיוק \( k \) כאלו. אז קל מאוד יהיה לשכנע אותנו שמ-\( s \) אי אפשר להגיע אל \( t \) תוך \( n \) צעדים באופן הבא: יתנו לנו כעדים \( k \) מסלולים, שכל אחד מוביל לצומת כלשהו שאינו \( t \), וכל הצמתים שונים אלו מאלו. זה יבטיח שלא ניתן להגיע מ-\( s \) אל \( t \) תוך \( n \) צעדים לכל היותר, כי יש בדיוק \( k \) צמתים שאפשר להגיע אליהם, ו”כיסינו” את כולם. כמה זכרון זה דורש? ובכן, כבר אמרנו שלבדוק מסלול דורש רק כמות לוגריתמית של זכרון. אבל, בעיה: איך נדע שכל \( k \) הצמתים שהביאו אותנו אליהם שונים זה מזה? בשביל זה צריך יהיה לזכור את כולם, וייתכן ש-\( k \) כבר יהיה גדול מדי מכדי להיות לוגריתמי (נניח, חצי מהצמתים בגרף). מה עושים?

הפתרון פשוט: העד יורכב מסדרה של טענות מהצורה “הצומת \( v \) ישיג מהצומת \( s \) לכל היותר ב-\( n \) צעדים, והרי הוכחה לכך…”, כאשר הסדר שבו מופיעות הטענות בתוך העד מתאים לסדר לקסיקוגרפי כלשהו שנקבע על הצמתים \( v \) (בסופו של דבר, צמתים, כמו כל מידע אחר, מיוצגים בידי מחרוזות בינאריות, ועל מחרוזות כאלו יש סדר באופן טבעי). בכל שלב נצטרך לזכור מה הצומת האחרון שעליו כבר הוכיחו שהוא ישיג מ-\( s \) ולבדוק אם החדש אכן גדול ממנו. אם הוא אכן גדול יותר, אפשר לשכוח את הקודם ולזכור רק את הנוכחי; אם הוא לא גדול יותר, אפשר להפסיק את בדיקת העד ולהכריז שמרמים אותנו. זה מבטיח שלא נספור אף צומת פעמיים, ולכן כל מה שצריך לשמור בנוסף הוא את מספר הצמתים שכבר שוכנענו שהם ישיגים מ-\( s \), וכדי לאחסן מספר שהוא לכל היותר מספר הצמתים הכולל בגרף דרוש רק זכרון לוגריתמי.

אז מה ראינו? שבזכרון לוגריתמי אפשר לבדוק הוכחה לטענה מהצורה “לפחות \( k \) הצמתים הללו ישיגים מ-\( s \) ב-\( n \) צעדים”, ושאם זה משולב בטענה מהצורה “בדיוק \( k \) צמתים ישיגים מ-\( s \) ב-\( n \) צעדים” אפשר להוכיח שמשהו לא ישיג מ-\( s \) ב-\( n \) צעדים. אבל איך אפשר להראות שבדיוק \( k \) צמתים ישיגים מ-\( s \) ב-\( n \) צעדים? ובכן, באינדוקציה על \( n \).

בואו נסמן ב-\( C_{n} \) את מספר הצמתים שישיגים מ-\( s \) לכל היותר ב-\( n \) צעדים. ראשית, ברור ש-\( C_{1} \) ניתן לחישוב באופן עצמאי לגמרי ובלי שום עזרה - פשוט עוברים איכשהו על רשימת הקשתות של הגרף וסופרים כמה מחוברות ל-\( s \). האתגר הוא להראות שאפשר לתת כעד את \( C_{n+1} \) באופן כזה שאם \( C_{n} \) כבר נתון, אפשר לבדוק שהעד נכון. איך עושים את זה?

בואו נעצור לרגע כדי לקחת אוויר ולסכם את מה שראינו עד כה. ראינו כי ניתן להוכיח (באופן שיהיה ניתן לבדיקה בזכרון לוגריתמי) שצומת כלשהו ישיג מ-\( s \) ב-\( n \) צעדים. כמו כן, ראינו כי אם \( C_{n} \) נתון, אז אפשר להוכיח שצומת כלשהו אינו ישיג מ-\( s \) ב-\( n \) צעדים. למעשה, אפשר גם להוכיח באופן דומה מאוד שצומת \( v \) אינו ישיג מ-\( s \) ב-\( n+1 \) צעדים - פשוט מוכיחים שאף שכן של \( v \) אינו ישיג מ-\( s \) ב-\( n \) צעדים (ולמי שנזקק לפירוט - ההוכחה כוללת את רשימת כל \( C_{n} \) השכנים שכן ישיגים ואת המסלול שמוביל להם; בזמן שבודקים שההוכחה נכונה גם בודקים שכל אחד מהשכנים הללו אינו שכן של \( v \)).

עכשיו בואו נעצור לרגע ונחשוב - איך כל המרכיבים הללו פותרים לנו את הבעיה של חישוב \( C_{n+1} \)? תנסו לחשוב על זה בעצמכם לרגע. תזכרו שאנחנו כלל לא צריכים להיות חסכוניים בזמן ריצה, רק בזכרון.

התשובה פשוטה: ההוכחה לערך החדש של \( C_{n+1} \) תהיה מורכבת מרשימת כל הצמתים בגרף לפני הסדר, כשאחרי כל צומת ההוכחה או טוענת שהוא ישיג מ-\( s \) ב-\( n+1 \) צעדים ומספקת תת-הוכחה שמראה זאת, או טוענת שהוא אינו ישיג מ-\( s \) ב-\( n+1 \) צעדים, ומספקת תת-הוכחה שמראה זאת. הגאונות כאן היא בכך שאחרי שאנחנו גומרים עם צומת, אנחנו לא צריכים לזכור אם הוא היה ישיג או לא היה ישיג (זה ידרוש מאיתנו הרבה יותר מדי זכרון לתחזק רשימה כזו) אלא רק להוסיף או לא להוסיף 1 למונה של \( C_{n+1} \) שאנחנו מתחזקים. אחרי שנסיים לקרוא את ההוכחה (שכאמור, אומרת פרטנית מה קורה לכל אחד מהצמתים בגרף), יהיה ברשותנו הערך הנכון של \( C_{n+1} \).

מכאן הפתרון לבעיה טריוויאלי. ההוכחה לכך ש-\( t \) לא ישיג מ-\( s \) ראשית כוללת הוכחות לסדרת הערכים \( C_{1},C_{2},\dots,C_{\left|V\right|} \), ולבסוף היא כוללת הוכחה לכך ש-\( t \) אינו ישיג מ-\( s \) ב-\( \left|V\right| \) צעדים, שמסתמכת על \( C_{\left|V\right|} \). אם \( t \) לא ישיג מ-\( s \) ב-\( \left|V\right| \) צעדים, הוא לא ישיג בכלל (למה?).

מה שיפה בהוכחה הזו היא השימוש האינטנסיבי משהו שהיא עושה ב”הוכחות”. אנחנו לא סתם מספקים מסלול וזהו, אלא לכל שלב של חישוב \( C_{i} \), אנחנו מספקים (שוב ושוב ושוב) את ההוכחה שצומת מסויים ישיג או לא ישיג מ-\( s \), לכל צומת בגרף. האינטנסיביות הזו מצליחה להניב בסיום פתרון שהוא מאוד חסכוני בזכרון (על משקל בזבוז אדיר של זמן הריצה, כמובן), וזה נראה מפתיע - ויותר מכך, מעלה את השאלה איך לעזאזל בכלל חשבו על פתרון כמו זה (אם כי אני חייב להודות - ביחס למשפט ברינגטון, משפט אימרמן עוד נראה מתבקש איכשהו). פרט לכך, המשפט הוא המחשה יפה מאוד לטעמי של האופן הכל כך שונה שבו סיבוכיות זכרון מתנהגת ביחס לסיבוכיות זמן.