שאלת מבחן במבוא למדעי המחשב - אוניברסיטת בן גוריון 2019 - מערכים

**סעיף ב (15 נקודות):** בהנתן מספר $n > 3$, נחפש השמה טובה למשתנים הפסוקיים $x_1, x_2, x_3, \ldots, x_n$. השיטה `public static void encode(int n)`: 1. מקבלת מספר $n > 3$ 2. מאתחלת פותרן של SAT 3. מוסיפה לפותרן את כל הפסוקיות הנדרשות כך שנוסחת ה-CNF המתקבלת תסופק אם ורק אם קיימת השמה טובה עבור הסידרה $x_1, x_2, x_3, \ldots, x_n$. השיטה encode לא פותרת את הנוסחה. היא רק מוסיפה את פסוקיותיה לפותרן. ניתן למצוא בנספח תזכורת לשיטות ולאופן השימוש ב SATSolver. לדוגמא: ידוע שקיים פתרון עבור סידרה באורך שמונה. קטע הקוד הבא משתמש בפונקציה encode: ```java public static void main(String[] args) { encode(8); boolean[] assignment = SATSolver.getSolution(); for (int i = 1; i <= 8; i = i + 1) System.out.print("x[" + i + "]=" + assignment[i] + " "); System.out.println(); } ``` לאחר שנריץ קטע קוד זה, תודפס השורה שמציינת סידרה טובה. לדוגמה, יתכן ותודפס השורה הבאה: x[1]=false x[2]=true x[3]=false x[4]=true x[5]=true x[6]=false x[7]=true x[8]=false

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

פתרון: המטרה היא לקודד את הבעיה של מציאת "השמה טובה" לנוסחת **CNF** (Conjunctive Normal Form), אותה ניתן להעביר ל**פותרן SAT**. משתנה פסוקי $x_i$ ייוצג על ידי המשתנה הבוליאני מספר `i` בפותרן. ליטרל חיובי `i` מייצג $x_i=\text{true}$ וליטרל שלילי `-i` מייצג $x_i=\text{false}$. על פי ההקשר והדוגמה, **"השמה טובה"** היא השמה שבה אין שלושה משתנים עוקבים עם אותו ערך אמת. כלומר, לכל $i$ בתחום $1 \le i \le n-2$, לא מתקיים התנאי $x_i = x_{i+1} = x_{i+2}$. כדי לאכוף אילוץ זה, עלינו לתרגם אותו לאוסף של פסוקיות (clauses). נוסחת CNF היא **AND** של פסוקיות, כאשר כל פסוקית היא **OR** של ליטרלים. פותרן SAT ימצא השמה שמספקת את כל הפסוקיות בו-זמנית. האילוץ "לא ייתכן כי $x_i = x_{i+1} = x_{i+2}$" מתפרק לשני מקרים שאותם יש למנוע עבור כל $i$ מ-1 עד $n-2$: 1. לא ייתכן כי $x_i, x_{i+1}, x_{i+2}$ כולם `true`. 2. לא ייתכן כי $x_i, x_{i+1}, x_{i+2}$ כולם `false`. כעת נתרגם כל אחד משני האיסורים הללו לפסוקית CNF: 1. כדי למנוע את המצב שבו $x_i, x_{i+1}, x_{i+2}$ כולם `true`, עלינו לדרוש שהפסוק $x_i \land x_{i+1} \land x_{i+2}$ יהיה שקרי. כלומר, אנו דורשים שהשלילה שלו, $\neg(x_i \land x_{i+1} \land x_{i+2})$, תהיה אמת. לפי **כלל דה-מורגן**, ביטוי זה שקול לפסוקית $\neg x_i \lor \neg x_{i+1} \lor \neg x_{i+2}$. בתחביר של הפותרן, פסוקית זו תיוצג על ידי הליטרלים `{-i, -(i+1), -(i+2)}`. 2. כדי למנוע את המצב שבו $x_i, x_{i+1}, x_{i+2}$ כולם `false`, עלינו לדרוש שהפסוק $\neg x_i \land \neg x_{i+1} \land \neg x_{i+2}$ יהיה שקרי. כלומר, אנו דורשים שהשלילה שלו, $\neg(\neg x_i \land \neg x_{i+1} \land \neg x_{i+2})$, תהיה אמת. לפי **כלל דה-מורגן**, ביטוי זה שקול לפסוקית $x_i \lor x_{i+1} \lor x_{i+2}$. בתחביר של הפותרן, פסוקית זו תיוצג על ידי הליטרלים `{i, i+1, i+2}`. לסיכום, הפונקציה `encode(n)` תעבור בלולאה על כל האינדקסים $i$ מ-1 עד $n-2$, ובכל איטרציה תוסיף לפותרן את שתי הפסוקיות הללו. כך נבטיח שכל פתרון שהפותרן ימצא יקיים בהכרח את האילוץ לכל שלשה של משתנים עוקבים.$\blacksquare$