ההוכחה הארוכה ביותר בהיסטוריה! (או: איך פותרי SAT מתגברים על בעיות קומבינטוריות, אבל היי זה שם פחות מפוצץ)

לפני חודש וקצת הצליחה תוצאה מתמטית נחמדה להיכנס אל החדשות לא בשל הסיבות שבגללן היא טובה, אלא בעיקר אלו שבגללן היא בעייתית: ההוכחה שלה היא (לכאורה) בגודל מפלצתי של 200 טרה-בייט. כמה זה הרבה? נאמר, זה פי 40 יותר מידע מאשר היה בשרתי ויקיפדיה ב-2010, ויש עוד שלל המחשות. בקיצור, זה הרבה מאוד. הנתון הזה מאוד הלהיב את העיתונים, וחלקם גם הגדילו לעשות וטענו ש”יקח 10 מיליארד שנים לקרוא את ההוכחה”. הנה כמה כתבות בעניין. בפוסט הזה אני אנסה להסביר מה בעצם נפתר, למה זה דרש הוכחה כזו ארוכה, ומה זה אומר על החיים, היקום ובכלל.

נתחיל מהתקציר. הבעיה מתעסקת במספרים טבעיים, \( 1,2,3,4,\dots \). שלושה מספרים כאלו \( a,b,c \) נקראים שלשה פיתגורית אם \( a^{2}+b^{2}=c^{2} \) (השם מגיע מכך שמשפט פיתגורס מוכיח שזה הקשר בין אורכי הצלעות של משולש ישר זווית). אנחנו יודעים הרבה דברים נחמדים על שלשות פיתגוריות, למשל שיטה יעילה לייצר את כולן, אז זה לא העניין. העניין הוא השאלה הבאה: נניח שיש לנו את קבוצת המספרים מ-1 עד \( n \) ואנחנו מחלקים אותה לשתי קבוצות שונות; האם בהכרח באחת מהקבוצות הללו תהיה לנו שלשה פיתגורית? בלשון ציורית מדברים לפעמים על צביעה - נניח שאנחנו צובעים כל מספר בקבוצה בכחול או באדום; האם תהיה לנו שלשה פיתגורית שכל שלושת המספרים שלה צבועים באותו הצבע?

הנה דוגמה. השלשה הפיתגורית הפשוטה ביותר היא \( 3,4,5 \). אם כן, נסתכל על הקבוצה \( \left\{ 1,2,3,4,5\right\} \). אם נחלק אותה לשתי קבוצות כך: \( \left\{ 1,2\right\} ,\left\{ 3,4,5\right\} \) הרי שבאחת מהקבוצות הללו באמת יש שלשה פיתגורית. לעומת זאת, אם נחלק אותה \( \left\{ 1,2,3\right\} ,\left\{ 4,5\right\} \) הרי שבחלוקה הזו אין לנו שלשה פיתגורית באף אחת מהקבוצות. כלומר, כאן היה קל למצוא חלוקה שבה אין שלשה פיתגורית באף קבוצה. ככל שנגדיל את \( n \) כך נגלה שנהיה לנו קשה יותר ויותר למצוא חלוקה שבה באף קבוצה אין שלשה פיתגורית (אינטואיטיבית, בגלל שככל שהקבוצה יותר גדולה כך יש יותר שלשות פיתגוריות שצריך יהיה להפריד). אם מתישהו נגיע אל \( n \) שבו אין שום דרך לחלק את המספרים מ1- עד \( n \) לשתי קבוצות כך שבאף אחת מהן אין שלשה פיתגורית, מובטח לנו שזה מה שיקרה מעתה והלאה ותמיד, לכל \( m\ge n \) (כי תמיד אפשר פשוט להתעלם מכל מספר שגדול מ-\( n \) ועדיין לקבל שלשה פיתגורית בכל חלוקה). לכן יש כאן שתי שאלות:

1. האם קיים \( n \) שעבורו לכל חלוקה לשתי קבוצות, באחת מהקבוצות יש שלשה פיתגורית?
2. אם קיים כזה, מה ה-\( n \) המינימלי?

המאמר עונה לשתי השאלות הללו: קיים \( n \) כזה, וה-\( n \) המינימלי הוא \( n=7825 \).

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

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

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

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

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

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

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

בואו נעבור עכשיו לדיון טיפה יותר טכני על הפרטים. כאמור, את כל המאמר אפשר לתמצת ל”המרנו את הבעיה לבעיית SAT ופתרנו את הבעיה הזו בצורה חכמה”. אז צריך להתחיל מהסבר מהי בעיית SAT. יש לי פוסט בנושא כאן עם ההגדרות המדויקות, אז לא אחזור עליהן כאן. השורה התחתונה היא זו: אם יש לנו את קבוצת המספרים \( \left\{ 1,2,\dots,n\right\} \) אנחנו מגדירים לכל מספר \( k \) בקבוצה משתנה \( x_{k} \) שיכול לקבל 0 או 1, כאשר הערך שהמשתנה מקבל אומר האם המספר \( k \) נמצא בקבוצה מס’ 0 או בקבוצה מס’ 1 בחלוקה שלנו את התחום לשתי קבוצות (כלומר, כל השמה של ערכים לכל המשתנים מגדירה לנו חלוקה של הקבוצה לשתי קבוצות). כעת לכל שלשה פיתגורית \( a^{2}+b^{2}=c^{2} \) של מספרים בין 1 ל-\( n \) אנחנו מגדירים נוסחה מהצורה \( \left(x_{a}\vee x_{b}\vee x_{c}\right)\wedge\left(\overline{x_{a}}\vee\overline{x_{b}}\vee\overline{x_{c}}\right) \). מה שהנוסחה הזו אומרת, מילולית, היא שעבור ההשמה שלנו למשתנים \( x_{a},x_{b},x_{c} \), לפחות אחד מהמשתנים קיבל 0 ולפחות אחד מהמשתנים קיבל 1. כלומר, לא כל המשתנים קיבלו אותו מספר; כלומר, לא כל שלושת המספרים \( a,b,c \) נמצאים באותה קבוצה; כלומר, השלשה \( a,b,c \) לא התקבלה. אם נמצא השמה למשתנים שנותנת ערך “אמת” לכל הנוסחאות הללו, עבור כל השלשות הפיתגוריות הרלוונטיות, אז מצאנו חלוקה של הקבוצה \( \left\{ 1,\dots,n\right\} \) שבה לא נוצרות שלשות פיתגוריות. כותבי המאמר עשו את זה והצליחו למצוא השמה כזו עבור \( n=7824 \), מה שאומר שהערך של \( n \) שעבורו לכל חלוקה יש שלשה פיתגורית הוא לפחות 7825.

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

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

כל מי שקצת מתעסק בתחום של פותרי SAT מבין מהר מאוד שיש לו כאן ביד כלי חזק ושימושי מאוד, וכל מי שאוהב קצת מתמטיקה כנראה מתחיל לחשוב על בעיות קומבינטוריות שאפשר לפתור. העניין הוא, כרגיל, שאם היה קל לפתור משהו, הוא כבר היה נפתר. כדי לפתור בעיה קומבינטורית פתוחה באמצעות פותרי SAT צריך לשלוט בצ’ופצ’יקים של קצה התחום, להיות עם מחשבים חזקים ואופטימיזציות חזקות. זו הסיבה למה אני, למשל, ממש לא קרוב לפתרון בעיות כאלו למרות שאני מכיר פותרי SAT. במובן הזה, המאמר מאוד מעניין - הוא סוג של Tour De Force של פתרון SAT. אבל זה שההוכחה יצאה מאוד ארוכה - זה הרבה פחות מעניין לטעמי (אורך ההוכחה הוא בסך הכל פונקציה של גודל הבעיה; היופי כאן הוא בכך שהצליחו בכלל למצוא הוכחה על בעיה גדולה כל כך). והתוצאה עצמה, וזה שזה יצא דווקא 7825 - גם זה לא נראה לי ממש מעניין. אולי בעתיד נסיק איזו תובנה מהותית מהמספר הזה, 7825; אבל בינתיים פרט למספר הזה ההוכחה לא מלמדת אותנו שום דבר חדש, וזו הסיבה שבגלל לא חשבתי שיש ממש טעם לכתוב פוסט בנושא מלכתחילה. אני מקווה שיצא פוסט מספיק מעניין בכל זאת.