רזולוציה - איך אפשר להוכיח שאי אפשר?

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

מהי רזולוציה? פשוט מאוד - זה כלל שבו משתי פסוקיות CNF מסיקים פסוקית חדשה. הכלל אומר כך: אם יש לי פסוקית \( C \) שבה מופיע משתנה \( x \), ויש לי פסוקית \( D \) שבה מופיע אותו המשתנה, אבל בשלילה - כלומר, היא כוללת את הליטרל \( \neg x \), אז אפשר לבנות משתי הפסוקיות הללו פסוקית חדשה (שלפעמים מסמנים \( C\otimes D \)) שכוללת את כל הליטרלים ב-\( C \) פרט ל-\( x \) וכל הליטרלים ב-\( D \) פרט ל-\( \neg x \).

כלומר, פורמלית, אם \( C=\left(x\vee l_{1}^{c}\vee\dots\vee l_{k}^{c}\right) \) ו-\( D=\left(\neg x\vee l_{1}^{d}\vee\dots\vee l_{t}^{d}\right) \) אז \( C\otimes D=\left(l_{1}^{c}\vee\dots\vee l_{k}^{c}\vee l_{1}^{d}\vee\dots\vee l_{t}^{d}\right) \).

חדי העין שביניכם אולי יתריעו כעת שהסימון בעייתי כי הוא לא מבהיר מה המשתנה שעל פיו עושים רזולוציה - אולי יש יותר ממשתנה אחד שמופיע בפסוק אחד ושלילתו מופיעה בשני? ובכן, אנחנו מניחים תמיד שברור מההקשר מה המשתנה הרלוונטי, אבל כשאהיה ממש ממש פורמלי אכתוב \( C\otimes_{x}D \) כדי שלא יהיה מקום לספק.

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

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

האמירה האחרונה אולי עשויה להישמע לכם חשודה, ובצדק - הטענה ש”אי אפשר לספק את הפסוקית הריקה” נשמעת קצת שרירותית. אם כן, חשבו לרגע איך רזולוציה יכולה בכלל ליצור את הפסוקית הריקה מלכתחילה: בהכרח אנחנו חייבים להפעיל אותה על שתי פסוקיות מהצורה \( C=\left(x\right) \) ו-\( D=\left(\neg x\right) \), כלומר פסוקיות שכוללות כל אחת רק ליטרל יחיד, שהוא של משתנה כלשהו באחת מהן, ושלילתו בשני. בבירור אף השמה אינה יכולה לספק את שתי הפסוקיות הללו בו זמנית, ולכן כבר כאן ברור ש”אי אפשר לספק את \( \varphi \)” (אם \( C,D \) נגזרו מ-\( \varphi \) על ידי רזולוציה). מכאן שהגיוני להגדיר את הפסוקית הריקה ככזו שאינה מסתפקת לאף השמה. עוד דרך לחשוב על זה היא זו: פסוקית מסתפקת על ידי השמה כלשהי אם קיים משתנה כלשהו שמקבל 1 תחת ההשמה הזו. אם אין משתנים בפסוקית, אז לא יכול להיות קיים משתנה כזה.

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

ההוכחה שמערכת ההוכחה שהצגתי היא אכן שלמה ונאותה הייתה די מורכבת, כך שלא סביר לצפות שרזולוציה תיתן לנו מערכת הוכחה חזקה באותה מידה בלי שנצטרך לעבוד די קשה לשם כך, אבל המטרות שלי בפוסט הזה הן צנועות יותר. הרעיון הוא כזה: מתחילים עם פסוק CNF \( \varphi \), שעליו חושבים בתור קבוצה של פסוקיות שהיא קבוצת ה”הנחות” שלנו. אחר כך בונים הוכחה שהיא סדרה של פסוקים שכל אחד מהם הוא פסוקית CNF שהיא הנחה או נובעת מקודמותיה על ידי רזולוציה. כלומר, גם פה יש לנו מערכת הוכחה מסוג הילברט, אבל ויתרנו על דרישת השלמות של המערכת ה”כללית” - יהיה די קל למצוא פסוקים שנובעים לוגית מ-\( \varphi \) אבל לא יכיחים ממנה במערכת. עם זאת, נאותות עדיין תתקיים - כל פסוק שמתקבל במערכת אכן ינבע לוגית מ-\( \varphi \), ותתקיים תכונת שלמות מוחלשת, שמספיקה לצרכינו: אם \( \varphi \) אינה ספיקה, אז \( \varphi\vdash\mbox{F} \) כאשר \( \mbox{F} \) הוא הסימון שלי לפסוקית הריקה שאינה כוללת ליטרלים. במילים פשוטות, אם \( \varphi \) לא ספיק המערכת תוכל להוכיח זאת, על ידי גזירה של הפסוקית הריקה. לכן אולי יותר נכון לחשוב על רזולוציה בתור “מערכת הפרכה” ולא מערכת הוכחה.

הבה ונוכיח את הטענה הזו. ההוכחה די קלה מבחינה רעיונית אבל הפרטים הטכניים יכולים להקשות על ההבנה שלה, אז בואו נתחיל מהרעיון. זוכרים איך במטריקס אמרו “Guns, lots of guns’’? אז כאן זה “רזולוציה, הרבה רזולוציה”. הרעיון הוא לעשות כמה רזולוציה שרק אפשר ובסוף \( \mbox{F} \) יהיה חייב לצוץ.

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

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

זה אולי נשמע נחמד ברמת נפנופי הידיים, אבל אני בהחלט מבין את מי שזה עדיין נראה לו חשוד. אז בואו נעבור לפורמליסטיקה. אני הולך לחשוב על כל פסוק CNF בתור קבוצה של פסוקיות. נניח ש-\( \varphi \) המקורי מכיל את המשתנים \( x_{1},\dots,x_{n} \), אז אני הולך להגדיר סדרה של פסוקי CNF \( \varphi_{0},\varphi_{1},\varphi_{2},\dots,\varphi_{n} \) כך ש-\( \varphi_{0}=\varphi \) ובאופן כללי \( \varphi_{k} \) מכיל רק את המשתנים עם אינדקס גדול מ-\( k \) (\( x_{k+1},\dots,x_{n} \)) ולכן בפרט \( \varphi_{n} \) לא יכול להכיל משתנים בכלל ומכאן שהוא או פסוק שמכיל פסוקית אחת, ריקה, ולכן אינו ספיק, או שהוא פסוק שאינו מכיל פסוקיות כלל, ולכן הוא טאוטולוגיה.

כדי להגדיר את \( \varphi_{k+1} \) מתוך \( \varphi_{k} \) אני הולך לחלק את הפסוקיות של \( \varphi_{k} \) לארבע קבוצות זרות ומשלימות: פסוקיות שבהן מופיעים גם \( x_{k} \) וגם \( \neg x_{k} \), כלומר הן טאוטולוגיות ואני הולך להתעלם מהן; פסוקיות שבהן לא \( x_{k} \) ולא \( \neg x_{k} \) מופיעים ואני הולך להעביר אותן כמות שהן ל-\( \varphi_{k+1} \) ; פסוקיות שבהן \( x_{k} \) מופיע אבל לא \( \neg x_{k} \), ופסוקיות שבהן \( \neg x_{k} \) מופיע אבל לא \( x_{k} \). בבירור אלו כל המקרים האפשריים. אז בואו נגדיר: \( \varphi_{k}=T_{k}\cup N_{k}\cup A_{k}\cup B_{k} \) כך ש-

\( T_{k}=\left\{ C\in\varphi_{k}\ |\ x_{k}\in C\wedge\neg x_{k}\in C\right\} \)

\( N_{k}=\left\{ C\in\varphi_{k}\ |\ x_{k}\notin C\wedge\neg x_{k}\notin C\right\} \)

\( A_{k}=\left\{ C\in\varphi_{k}\ |\ x_{k}\in C\wedge\neg x_{k}\notin C\right\} \)

\( B_{k}=\left\{ C\in\varphi_{k}\ |\ x_{k}\notin C\wedge\neg x_{k}\in C\right\} \)

עכשיו נגדיר את \( A_{k}\otimes B_{k} \) בתור “מה שמקבלים כשעושים את כל הרזולוציות שרק אפשר עם \( A_{k},B_{k} \)”:

\( A_{k}\otimes B_{k}=\left\{ C\otimes_{x_{k}}D\ |\ C\in A_{k},D\in B_{k}\right\} \)

ועכשיו נגדיר:

\( \varphi_{k+1}=N_{k}\cup A_{k}\otimes B_{k} \)

כלומר, זרקנו לפח את כל הפסוקיות שהיו טאוטולוגיות ב-\( \varphi_{k} \), זרקנו לפח את כל הפסוקיות שהכילו את \( x_{k} \) בצורה זו או אחרת, ובתור פיצוי הכנסנו פנימה את התוצר של כל הרזולוציות של פסוקיות ב-\( A_{k},B_{k} \). מצד אחד, \( \varphi_{k+1} \) יכול להיות הרבה יותר מסובך מ-\( \varphi_{k} \) במובן זה שהוא יכיל הרבה יותר פסוקיות; מצד שני, הוא יו תר פשוט מ-\( \varphi_{k} \) במובן זה שהפסוקיות שלו כוללות משתנה אחד פחות - לא כוללות את \( x_{k} \).

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

איזו השמה מספקת את \( \varphi_{n} \) שאין בו בכלל משתנים? ובכן, לא תאהבו את זה אבל ההשמה הריקה - השמה שלא נותנת ערך לאף משתנה. אם זה מפריע לכם, אפשר לתקן את הניסוח ל”כל השמה למשתנים \( x_{1},\dots,x_{n} \) מספקת את \( \varphi_{n} \)” וזה תקין באותה המידה, אבל אני מעדיף מבחינה רעיונית לדבר על השמה ריקה. עכשיו, בואו נניח שיש לנו השמה \( \tau \) שמספקת את \( \varphi_{k} \) ומוגדרת רק עבור המשתנים \( x_{k+1},\dots,x_{n} \) (או לחילופין, לא משנה איך נגדיר אותה עבור \( x_{1},\dots,x_{k} \), עדיין נקבל שהיא מספקת את \( \varphi_{k} \)). עכשיו השאלה שעומדת בפנינו היא זו: איך נקבל מתוך \( \tau \) השמה שמספקת את \( \varphi_{k-1} \)?

יש בסך הכל שתי השמות שנראות כמו מועמדות מתאימות לספק את \( \varphi_{k-1} \) - אקרא להן \( \tau_{0},\tau_{1} \). הן זהות ל-\( \tau \) על המשתנים \( x_{k+1},\dots,x_{n} \) שעליהם \( \tau \) מוגדרת, ונבדלים בהגדרתם על \( x_{k} \): \( \tau_{0}\left(x_{k}\right)=0 \) ו-\( \tau_{1}\left(x_{k}\right)=1 \). עכשיו אני רוצה לטעון שלפחות אחת מההשמות הללו מספקת את \( \varphi_{k-1} \) - לשם כך אני אניח בשלילה שאף אחת מהן לא מספקת את \( \varphi_{k-1} \) ואסיק מכך שלא ייתכן ש-\( \tau \) סיפקה את \( \varphi_{k} \).

מה זה אומר ש-\( \tau_{0} \) אינה מספקת את \( \varphi_{k-1} \)? זה אומר שקיימת פסוקית \( C\in\varphi_{k-1} \) שאותה \( \tau_{0} \) אינה מספקת, כלומר לא קיים ליטרל ב-\( C \) ש-\( \tau_{0} \) נותנת לו 1. עכשיו, לא ייתכן ש-\( C\in T_{k-1} \) כי ב-\( T_{k-1} \) היו רק טאוטולוגיות שמסתפקות על ידי כל השמה. כמו כן, אם \( C\in N_{k-1} \) אז על פי הגדה, \( C\in\varphi_{k} \) ו-\( C \) לא כוללת ליטרל עבור המשתנה \( x_{k} \) ולכן \( \tau \) נותנת ל-\( C \) אותו ערך כמו \( \tau_{0} \), כלומר \( \tau \) אינה מספקת את \( C \) ולכן לא מספקת את \( \varphi_{k} \), כפי שרצינו. אז סיימנו גם עם המקרה הזה. לבסוף, האם ייתכן ש-\( C\in B_{k-1} \)? שוב לא, כי אם \( C\in B_{k-1} \) אז \( C \) היא מהצורה \( C=\left(\neg x_{k}\vee l_{1}\vee\dots\vee l_{t}\right) \) ולכן \( \tau_{0} \) מספקת את הליטרל \( \neg x_{k} \) של \( C \). מסקנה: בהכרח \( C\in A_{k-1} \).

בדיוק באותו האופן, מכך ש-\( \tau_{1} \) אינה מספקת את \( \varphi_{k-1} \) אנחנו מסיקים שקיימת פסוקית \( D\in B_{k-1} \) שאינה מסתפקת על ידי \( \tau_{1} \). עכשיו מגיע הפאנץ’: בואו נסתכל על \( C\otimes D \). זו פסוקית ששייכת ל-\( \varphi_{k} \), מה שאומר ש-\( \tau \) מספקת אותה. אבל זה בלתי אפשרי: על כל המשתנים שאינם \( x_{k} \), ההשמה \( \tau \) זהה להשמות \( \tau_{0},\tau_{1} \), וההשמות הללו נותנות 0 לכל הליטרלים ב-\( C,D \) למעט \( x_{k},\neg x_{k} \) שאינם מופיעים ב-\( C\otimes D \). הגענו לסתירה, והמסקנה היא שלפחות אחת מבין שתי ההשמות \( \tau_{0},\tau_{1} \) מספקת את \( \varphi_{k-1} \), וזה משלים את האינדוקציה ואת ההוכחה כולה.

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

מציאה של הוכחה קצרה בפרט גם דורשת שההוכחה עצמה תהיה קצרה, כך שהשאלה השניה היא חזקה יותר מהראשונה ופחות סביר שהתשובה לה תהיה חיובית: אם התשובה חיובית אז אפשר יהיה להכריע את בעיית SAT בזמן יעיל, מה שגורר ש-P=NP, וזו תוצאה מאוד לא סבירה. מצד שני, אולי יש הוכחות קצרות אבל פשוט אי אפשר למצוא אותן בזמן יעיל? כאן כדי להשוות את זה לבעיה ה”משלימה” - בהינתן פסוק CNF ספיק, האם יש לכך הוכחה קצרה? כאן התשובה היא בוודאי חיובית: ההשמה שמספקת את הפסוק כוללת בסך הכל \( n \) ביטים, אחד לכל משתנה. אז זו דוגמה לבעיה שבה יש הוכחה קצרה אבל כנראה (אם P שונה מ-NP) אין אלגוריתם יעיל שמוצא אותה.

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

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