מה זו בעיית SAT ולמה חשוב לפתור אותה?

אני רוצה לדבר על בעיה לא פתירה, ואיך שפותרים אותה.

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

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

פורמלית, אנחנו מתחילים ממשתנים. משתנה \( x \) הוא משהו שיכול לקבל שני ערכים - "אמת" ו"שקר", שאעדיף לסמן ב-1 ו-0 לצורך פשטות. עכשיו, ליטרל (שאני מסמן לרוב ב-\( l \)) הוא או משתנה או שלילה של משתנה, שאני מסמן ב-\( \neg x \). שלילה פירושה שאם \( x \) קיבל 0, אז \( \neg x \) קיבל 1, ואם \( x \) קיבל 1 אז \( \neg x \) מקבל 0.

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

לבסוף, פסוק CNF מורכב מאוסף פסוקיות שמחוברות עם קשר "וגם": \( \varphi=C_{1}\wedge C_{2}\wedge\dots\wedge C_{n} \). פסוק מסתפק על ידי השמה רק אם ההשמה מספקת את כל הפסוקיות שלו בו זמנית. ה-CNF שבשם מגיע מ-Conjunctive Normal Form - זה מרמז שיש דרכים אחרות לכתוב בהן פסוקים, ועוד נדון על כך בהמשך, אבל בבעיית SAT מתעסקים רק עם פסוקית בצורת CNF.

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

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

התשובה, כמובן, היא שאפשר למדל בעיות רבות ושונות בעזרת פסוקי CNF שכאלו. לכן תיארתי מלכתחילה את הבעיה בתור "נתון לנו אוסף של אילוצים" בלי בכלל לדבר על CNF. הנה דוגמה פשוטה לאופן שבו זה עובד: אנחנו רוצים לבנות מערכת שעות. יש לנו רשימה של קורסים שאנחנו צריכים לקחת; לכל קורס יש מספר קבוצות הרצאה שונות שאליהן ניתן ללכת. אנחנו רוצים לבנות מערכת ללא התנגשויות - כלומר, כך שאנחנו לא הולכים לשתי קבוצות הרצאה של קורסים שונים שהם באותה שעה. זו בעיה קלאסית עבור תרגום ל-CNF: לכל קורס יהיו לנו משתנים שמתארים "האם אני הולך לקבוצה שמספרה כך וכך של הקורס". כלומר, יהיו לנו משתנים \( x_{1},\dots,x_{n} \) עבור קורס בעל \( n \) קבוצות הרצאה שונות, כך שאם המשתנה \( x_{i} \) מקבל 1 המשמעות היא "אני הולך לקבוצה \( i \) של הקורס" ואם המשתנה \( x_{i} \) מקבל 0 המשמעות היא "אני לא הולך לקבוצה \( i \) של הקורס". אנחנו רוצים להוסיף ל-CNF את האילוץ "אנחנו הולכים לפחות לאחת מקבוצות ההרצאה"; לשם כך נוסיף לו את הפסוקית \( \left(x_{1}\vee x_{2}\vee\dots\vee x_{n}\right) \). כמו כן, אנחנו רוצים להוסיף לו את האילוץ "אנחנו לא הולכים לשתי קבוצות הרצאה שונות של אותו מקצוע (זה יהיה פשוט מטופש!). את זה אפשר לקודד על ידי אוסף פסוקיות: לכל \( i\ne j \), נוסיף את הפסוקית \( \left(\neg x_{i}\vee\neg x_{j}\right) \) שאפשר לקרוא בתור "או שאני לא הולך לקבוצה \( i \) או שאני לא הולך לקבוצה \( j \), או שניהם" - שמבטיח שאני לא הולך לפחות לאחת מהקבוצות הללו (כך שאם אני הולך לשתי קבוצות, הפסוקית עם המשתנים עבור שתיהן לא תסתפק). למי שעדיין לא רואה את זה, אפשר לחשוב על \( \left(\neg x_{i}\vee\neg x_{j}\right) \) כשקול לוגית לפסוק (שאינו פסוקית CNF) הבא: \( x_{i}\to\neg x_{j} \), שאומר "אם אני הולך לקבוצה \( i \), אז אני לא הולך לקבוצה \( j \)", וגם לפסוק \( x_{j}\to\neg x_{i} \).

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

מה עוד חסר? עוד אין לי ב-CNF שום אילוץ שמבטיח ששתי קבוצות הרצאה של קורסים שונים אינן מתנגשות. לשם כך אני צריך, כשאני בונה את ה-CNF, לעבור ידנית על כל שעות ההרצאה של כל הקורסים ולבדוק אם יש התנגשות. אם אני מוצא התנגשות בין הקבוצה שמתוארת על ידי המשתנה \( x_{i} \) והקבוצה שמתוארת על ידי המשתנה \( y_{j} \) (האות השונה מרמזת שמדובר על קורס שונה), אז אני מוסיף ל-CNF שלנו את הפסוקית \( \left(\neg x_{i}\vee\neg y_{j}\right) \), שמבטיחה שאני לא הולך לשתי קבוצות ההרצאה הללו בו זמנית. עכשיו הפסוק שבניתי הוא ספיק אם ורק אם קיימת מערכת שעות ללא התנגשויות, וכל השמה מספקת שלו ניתנת לתרגום למערכת שעות שכזו. זו המשמעות של מידול.

אפשר למדל עם פסוקי CNF עוד שלל בעיות רבות ושונות. אחד מהמשפטים המרכזיים בתורת החישוביות, משפט קוק-לוין, קובע שבעצם כל בעיה ב-NP ניתן למדל בעזרת פסוקי CNF באופן שבו הפסוק המתקבל הוא מסדר גודל "סביר" לעומת הבעיה המקורית (פולינומי). למקרה שאתם תוהים מה זה NP - אלו בעיות שעבורן ניתן לבדוק ביעילות האם פתרון מוצע הוא נכון. למשל, מערכת שעות (נותנים לכם מערכת שעות? פשוט תסתכלו עליה ותוודאו שאין התנגשויות, לא ייקח יותר מדי זמן). עם זאת, משפט קוק-לוין הוא תוצאה תיאורטית, במובן זה ששיטת הקידוד שהוא מציע היא מאוד מסורבלת. אם ניקח את משפט קוק-לוין ונפעיל אותו על בעיית מערכת השעות, לא נקבל קידוד אלגנטי כמו שתיארתי לעיל; נקבל קידוד מסובך פי כמה וכמה. וזה בעייתי מאוד, בהתחשב בכך שאנחנו רוצים גם לפתור את בעיית ה-SAT שמתקבלת מהקידוד. לכן חלק מהאומנות שבעבודה עם SAT היא לבצע את הקידוד המדובר בצורה חכמה. כדאי להעיר שלא תמיד כדאי לקודד את הבעיה דווקא עם SAT; תחום שלם במדעי המחשב מתעסק עם מה שנקרא CSP, שזה בעברית פשוט Constraint Satisfaction Problems - "בעיות סיפוק אילוצים" - שהן מעין הכללה של SAT בשלל דרכים שונות. לא אכנס לנושא הזה בכלל כרגע, למרות שהוא מרתק בפני עצמו; המטרה העיקרית שלי היא לדבר על איך פותרים את SAT, לא איך פותרים בעיות אחרות בעזרת SAT.

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

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