פותרים את SAT - אלגוריתם DPLL

הגענו סוף סוף לדבר על האופן שבו פותרים את בעיית SAT במקרה הכללי. יש לנו פסוק CNF \( \varphi \) ואין לו בהכרח צורה “נחמדה” כמו בבעיות 2SAT או HORNSAT שראינו בפוסט הקודם - מה עושים?

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

עכשיו בואו נעבור לתאר את האלגוריתם הבסיסי של התחום - כל כך בסיסי עד שרוב האלגוריתמים שמשתמשים בהם בימינו עדיין מבוססים על המבנה שלו ופשוט מרחיבים ומשפרים את השלבים. האלגוריתם נקרא DPLL על שם ממציאיו: D הוא מרטין דיוויס, שכבר הזכרתי בהקשר של הבעיה העשירית של הילברט; P הוא הילארי פוטנאם, שמפורסם מאוד בעיקר כפילוסוף ולוגיקאי; ו-LL הם ג’ורג’ לוגמן ודיוויד לאבלנד שאין לי מושג מי הם. היסטורית דיוויס ופוטנאם המציאו את האלגוריתם ולוגמן ולאבלנד שיפרו אותו, אבל לא ניכנס לפרטים הללו כאן.

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

עכשיו בואו נבין מה כל מושג כאן אומר.

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

“השמה במשתנה טהור” (Pure Variable Assignment) אומרת את הדבר הבא: נניח שיש לנו משתנה \( x \) כך שבכל פסוקית שבה הוא מופיע זה תמיד בתור \( x \) ואף פעם לא בתור השלילה \( \neg x \). זה המובן של “טהור”, אבל כדי שלא להיות גזענים כלפי ליטרלים גם אם הליטרל \( \neg x \) מופיע בכל הפסוקיות שבהן מופיע המשתנה \( x \) ואילו הליטרל \( x \) לא מופיע אף פעם נאמר ש-\( x \) טהור. במקרה שבו כל המופעים של \( x \) הם חיוביים (כלומר, הוא מופיע בתור הליטרל \( x \)) אנחנו יכולים רק להרוויח מכך שנציב ב-\( x \) את הערך 1 - זה יספק מיידית את הפסוקיות שבהן \( x \) הופיע, ושאר הפסוקיות יוותרו ללא שינוי (בעוד שאם \( \neg x \) היה מופיע בפסוקית כלשהי זה היה משנה אותה לרעה - היא הייתה “מאבדת” ליטרל). בדומה, אם כל המופעים של \( x \) הם שליליים בתור הליטרל \( \neg x \), אפשר רק להרוויח מכך שנציב ב-\( x \) 0, ולכן עושים זאת. אחרי ההצבה הזו ייתכן שאחד המשתנים שקודם לא היה טהור יהפוך לטהור (כי “חיסלנו” את כל הפסוקיות שבהן הופיע מופע שלילי שלו ונותרו רק המופעים החיוביים, למשל) ולכן גם כאן התהליך יכול להימשך כמה פעמים.

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

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

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

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

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

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

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

לבסוף, החלק המשמעותי ביותר שאפשר לטפל בו בצורה שונה הוא זה של החזרה לאחור עם זיהוי כשלון. בשנים האחרונות מאוד פופולרית גישה שונה ומתוחכמת יותר לטיפול בשלב הזה מאשר זו של DPLL - גישה חשובה מספיק כדי לזכות לשם משל עצמה - Conflict Driven Clause Learning, ובקיצור CDCL. את הרעיון המלא יחסית אציג בפוסט הבא, אז בינתיים טיזר: שני הדברים המרכזיים שהאלגוריתם עושה באופן שונה מ-DPLL הן שהוא לא חוזר צעד אחד אחורה אל משתנה הבחירה האחרון אלא יכול לחזור כמה וכמה רמות אחורה, ושכאשר הוא “נתקע” הוא מנתח את מה שהשתבש ולומד מזה פסוקית חדשה שאותה הוא מוסיף לפסוק שהוא מנסה לפתור. באופן מעניין למדי זה “חוסך” לו את הצורך לבצע ניהול חשבונות עבור משתני הבחירה - האלגוריתם לא צריך “להפוך” את הערך של משתנה בחירה בשום שלב, זה כבר נובע מעצמו מהדברים שהוא למד. כאמור, אדבר על זה בפוסט הבא.

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