פותרים את SAT: המקרים של HORNSAT ו-2SAT

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

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

נתחיל עם בעיה שנקראת HORNSAT, על שם הלוגיקאי אלפרד הורן. בבעיה הזו נתון לנו CNF מצורה מיוחדת מאוד: כל פסוקית שלו מכילה לכל היותר ליטרל חיובי אחד - כל יתר הליטרלים הם בשלילה. פסוקית כזו נקראת פסוקית הורן. למשל, \( \left(\neg x\vee y\vee\neg z\vee\neg w\right) \) היא פסוקית הורן; גם \( \left(\neg x\vee\neg y\right) \) שאין בה בכלל ליטרלים חיוביים היא פסוקית הורן.

בואו נסתכל לרגע על הפסוקית \( \left(\neg x\vee y\vee\neg z\vee\neg w\right) \). אם נציב 0 ב-\( x \), או 0 ב-\( z \), או 0 ב-\( w \), זה יספק את הפסוקית. אבל מה יקרה אם נציב 1 בשלושתם? במקרה זה, כדי לספק את הפסוקית אנחנו חייבים להציב 1 ב-\( y \). כלומר, הפסוקית ממדלת טענה מהצורה “אם \( x,w,z \) מתקיימים כולם אז גם \( y \) מתקיים”. פורמלית כותבים את זה כך: \( \left(x\wedge w\wedge z\to y\right) \). באופן כללי, את הקשר \( \to \) אפשר “לקודד” עם שלילה ו-\( \vee \): \( \alpha\to\beta \) שקול לוגית ל-\( \neg\alpha\vee\beta \), ומכאן האופן שבו פסוקית כמו \( \left(x\wedge w\wedge z\to y\right) \) מוצגת כ-CNF. עם זאת, אני חושב שהרבה יותר קל להבין פסוקיות הורן כשחושבים עליהן כעל משהו מהצורה \( \left(x\wedge w\wedge z\to y\right) \).

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

מה זה אומר “חייב” לקבל 1? זה אומר שאם הוא לא מקבל 1, תהיה לנו פסוקית שאינה מסתפקת. אבל כדי שהדרך היחידה לספק פסוקית CNF היא על ידי הצבת 1 במשתנה \( x \) כלשהו, הפסוקית חייבת להיות מהצורה \( \left(x\right) \) (כי אם היה בה ליטרל נוסף, היינו מקבלים דרכים נוספות לספק את הפסוקית). פסוקית כזו נקראת פסוקית יחידה (Unit clause).

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

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

אחרי שגמרנו עם \( x \), צריך לבדוק אם יש לנו עוד פסוקיות יחידה חיוביות. ייתכן שקודם לא היו כאלו אבל הן נוצרו במהלך הפעפוע (למשל, אם קודם הייתה לנו הפסוקית \( \left(\neg x\vee y\right) \)). אם כן, מפעפעים גם את המשתנה החדש, וכן הלאה וכן הלאה. אם אין עוד פסוקיות יחידה חיוביות, אז כאמור פשוט מציבים 0 בכל המשתנים שנותרו וסיימנו.

האלגוריתם הזה ממש, ממש פשוט. בביצוע נאיבי זמן הריצה שלו הוא \( O\left(n^{2}\right) \), אבל עם קצת התחכמויות אפשר גם לבצע אותו בזמן לינארי (\( O\left(n\right) \)) מה שאומר שהוא גם יעיל מאוד. זה מעניין, כי מצד שני זו גם בעיה שהיא במובן מסויים “הכי קשה ב-P’’ (כאן P מייצג את אוסף הבעיות עם אלגוריתם פולינומי שפותר אותן), במובן זה שכל בעיה אחרת שיש אלגוריתם פולינומי המכריע אותה ניתנת לתרגום ל-HORNSAT תוך שימוש בכמות קטנה יחסית של זכרון - פולי-לוגריתמית (כלומר, כמות זכרון שהיא פולינום בלוגריתם של \( n \)). פורמלית אומרים שזו שפה שהיא P-שלמה (כמו שיש NP-שלמה) ביחס לרדוקציות logspace (ולכן, למשל, אם קיים אלגוריתם שפותר אותה בזכרון פולי-לוגריתמי - לא סביר בכלל - אז לכל שפה ב-P קיים אלגוריתם עם דרישות זכרון מצומצמות שכאלה).

בואו נעבור עכשיו לוריאנט אחר של SAT, שנקרא 2SAT. הפעם אנחנו מרשים לליטרל חיובי להופיע פעמיים בתוך פסוקית, אבל מטילים על הפסוק מגבלה די קשיחה: בכל פסוקית יש בדיוק שני ליטרלים (אנחנו מרשים גם פסוקיות כמו \( \left(x\vee x\right) \) שהן בפועל פסוקית עם ליטרל יחיד). ייתכן שהמגבלה הזו נראית לנו קשיחה מדי, כי אנחנו מגבילים את המספר המקסימלי של ליטרלים שיכולים להופיע בתוך פסוקית, אבל האינטואיציה שלנו בעייתית בהקשר הזה: וריאנט אחר הוא 3SAT שבו כל פסוקית מכילה בדיוק שלושה ליטרלים, ומסתבר שאפשר לקודד כל פסוק CNF כפסוק 3CNF במחיר של הגדלה לא משמעותית (לינארית באורך הכולל של הפסוקיות בפסוק המקורי) של גודל הפסוק. כך שהמגבלה פחות קטלנית מאשר היא נראית במבט ראשון, ועדיין - פסוקי 2CNF הם משמעותית יותר פשוטים ולכן אני יכול להציג אלגוריתם יעיל שבודק את הספיקות שלהם.

הסיבה שבגללה פסוקי 2CNF הם פשוטים ברמה שעוזרת לנו היא שאפשר לחשוב על כל פסוק כזה בתור אוסף אילוצים מהצורה “ליטרל אחד גורר ליטרל אחר”. את \( \left(x\vee y\right) \) אפשר לכתוב גם כ-\( \neg x\to y \) וגם כ-\( \neg y\to x \), כלומר כל פסוקית נותנת לנו שתי גרירות שמערבות ליטרלים. היופי פה הוא שגרירה היא יחס טרנזיטיבי: אם \( x\to y \) ו-\( y\to z \) אז גם \( x\to z \) גם אם הם לא מופיעים יחד באף פסוקית (אם תחשבו על זה לרגע, תראו שזה בעצם כלל הרזולוציה בתחפושת: מ-\( \left(\neg x\vee y\right) \) ו-\( \left(\neg y\vee z\right) \) אנו מסיקים את \( \left(\neg x\vee z\right) \)).

עכשיו, נניח שעל ידי שרשרת של הסקות כאלו קיבלנו את הגרירה \( x\to\neg x \). מה זה אומר? זה אומר שאם \( x \) שווה 1 אז גם \( \neg x \) צריך להיות שווה 1, אבל זה כמובן בלתי אפשרי, והמסקנה היא ש-\( x \) חייב לקבל 0 על ידי כל השמה שאנחנו מקווים שתספק את הפסוק שלנו (\( x\to\neg x \) הוא פשוט הפסוקית \( \left(\neg x\vee\neg x\right) \) בתחפושת, כלומר פסוקית היחידה \( \left(\neg x\right) \)).

ומה קורה אם קיבלנו גם את \( x\to\neg x \) וגם את \( \neg x\to x \)? הגרירה הראשונה מראה ש-\( x \) לא יכול לקבל 1, והשניה מראה ש-\( x \) לא יכול לקבל 0, ולכן המשחק נגמר - הפסוק אינו ספיק. במונחי רזולוציה, קיבלנו את \( \left(x\right),\left(\neg x\right) \) ואחרי רזולוציה לשניהם נקבל את הפסוקית הריקה. אם כן, יש לנו קריטריון להכרעה מתי פסוק 2CNF אינו ספיק: אם קיימת שרשרת גרירות מ-\( x \) אל \( \neg x \) וקיימת שרשרת גרירות מ-\( \neg x \) אל \( x \) עבור משתנה \( x \) כלשהו. מה שיפה כאן הוא שהקריטריון הזה הוא קריטריון של אם ורק אם: אם לאף משתנה אין שתי שרשראות גרירה כאלו, הפסוק ספיק. בואו נוכיח את זה.

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

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

תהליך הפעפוע יכול להסתיים בשתי דרכים שונות: או שניוותר לבסוף בלי פסוקיות יחידה, ואז נוכל לבחור משתנה חדש ולהציב בו ערך (אם עוד יש כזה שטרם הצבנו בו ערך), או שנגיע לפסוקית ריקה ולסתירה. אני רוצה לשכנע אתכם שאי אפשר להגיע לפסוקית ריקה. כדי להגיע לפסוקית ריקה, צריכים להיות שני ליטרלים \( l_{1},l_{2} \) כך ש-\( \left(l_{1}\vee l_{2}\right) \) היא פסוקית של \( \varphi \), ובנוסף לכך \( x\to\neg l_{1} \) ו-\( x\to\neg l_{2} \).

עכשיו, שימו לב לתעלול הבא: אם \( \left(l_{1}\vee l_{2}\right) \) היא פסוקית של \( \varphi \), אז למאגר הגרירות שלנו אפשר להוסיף את \( \neg l_{1}\to l_{2} \). כעת, מכיוון ש-\( x\to\neg l_{1} \) נקבל \( x\to l_{2} \). שקול לוגי של הפסוק הזה הוא \( \neg l_{2}\to\neg x \) (בדקו זאת!) ומכיוון ש-\( x\to\neg l_{2} \) נסיק \( x\to\neg x \), אבל הנחנו שזה לא קורה - סתירה! לכן תהליך הפעפוע לא יכול להיגמר עם פסוקית ריקה, וההצלחה של האלגוריתם מובטחת.

עד כאן התיאוריה, אבל איך מבצעים את האלגוריתם בפועל? ובכן, צריך למצוא משתנה \( x \) שאינו גוזר את \( \neg x \), צריך להציב בו ובכל מה שנגזר ממנו 1, ולוודא שלא נגרמו בעיות בשל כך. הדרך הנוחה לחשוב על זה (וגם לממש בפועל) היא בתור אלגוריתם שפועל על גרף מכוון. הצמתים של הגרף יהיו הליטרלים של הפסוק שלנו, כלומר כל צומת הוא מהצורה \( x \) או מהצורה \( \neg x \) עבור משתנה \( x \) כלשהו, והקשתות מייצגות גרירה: אם \( \left(l_{1}\vee l_{2}\right) \) היא פסוקית ב-\( \varphi \), אז מוסיפים לגרף את הקשתות \( \neg l_{1}\to l_{2} \) ו-\( \neg l_{2}\to l_{1} \). כעת יש לנו פירוש פשוט לכך שליטרל אחד נגרר על ידי אחר: נסתכל על צומת \( l \) ואז נסתכל על כל צומת שישיג ממנו, כלומר שיש מסלול מכוון ממנו אליו. כל הצמתים הללו מייצגים ליטרלים שנובעים מ-\( l \).

כעת האלגוריתם ברור: בוחרים משתנה \( x \) באופן שרירותי, ומריצים עליו אלגוריתם DFS, שמוצא את כל הצמתים הישיגים ממנו. אם \( \neg x \) הוא לא בין הצמתים שהיו ישיגים מ-\( x \), אז מציבים 1 ב-\( x \) ובכל ליטרל אחר שצץ במהלך ה-DFS. לא ייתכן שנצטרך להציב 1 גם בליטרל וגם בשלילתו, כי כפי שכבר ראינו, זה היה גורם לכך שמ-\( x \) כן אפשר יהיה להגיע אל \( \neg x \).

אם כן ראינו שאפשר להגיע אל \( \neg x \) מתוך \( x \), אז נריץ DFS חדש מ-\( \neg x \) ונפעל באותו האופן כמו קודם. אם הגענו אל \( x \) במהלך ה-DFS אפשר לסיים - זו הוכחה שהפסוק לא ספיק (וקל לזקק ממנה הוכחת רזולוציה אמיתית).

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

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

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