הועלה לאתר:  
מספר עמודים: 120
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

6.8.2. אלגוריתם בסיסי לפתרון SAT -Davis Putmam (DPLL), 1960, 1962

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

לדוגמא, תחת ההשמה plot:$b = 1,c = 0$ הפסוקית הבאה היא פסוקית יחידה: plot:$\left( {a \vee \neg b \vee c} \right)$. הדרך היחידה להרחיב את ההשמה הנתונה להשמה מספקת היא לתת לליטרל שנותר את הערך true.



האלגוריתם לפתרון SAT:

  1. מתחילים מהשמה חלקית ריקה - שלא נותנת ערך לאף משתנה.
  2. החלטה: מרחיבים את ההשמה החלקית הנתונה ע"י החלטה (משתנה + ערך).
  3. הסקה (BCP): מרחיבים השמה עם כל הגרירות שנובעות מההחלטה.
  4. ניתוח: אם התקבל קונפליקט (פסוקית קיבלה ערך F או לחילופין משתנה שחייב לקבל גם ערך true וגם ערך false) בהשמה הנוכחית אז מבצעים נסיגה, שבה מבטלים חלק מההחלטות, וחוזרים ל-1.

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

עצירת האלגוריתם:

  • האלגוריתם עוצר בהצלחה (עם השמה מספקת) כאשר נמצאה השמה שמספקת את כל הפסוקיות.
  • האלגוריתם עוצר ללא הצלחה (עם מסקנה שהנוסחה אינה ספיקה) אם יש פסוקית שערך האמת שלה הוא F ואין החלטות שאפשר לשנות אותן.

דוגמא לתהליך:

  1. נביט בנוסחה הפסוקית הבאה:

plot:$\left( {\neg b \vee c} \right) \wedge \left( {\neg a \vee \neg d} \right) \wedge \left( {a \vee b \vee \neg c} \right) \wedge \left( {\neg a \vee d} \right) \wedge \left( {a \vee \neg c \vee \neg e} \right)$

  1. החלטה ברמה 1: נבחר plot:$b = 1$:

plot:$\left( {\underbrace {\neg b}_0 \vee c} \right) \wedge \left( {\neg a \vee \neg d} \right) \wedge \left( {a \vee \underbrace b_1 \vee \neg c} \right) \wedge \left( {\neg a \vee d} \right) \wedge \left( {a \vee \neg c \vee \neg e} \right)$

  1. BCP: צריך לבצע plot:$c = 1$ בגלל פסוקית היחידה השמאלית:

plot:\[\left( {\underbrace {\neg b}_0 \vee \underbrace c_1} \right) \wedge \left( {\neg a \vee \neg d} \right) \wedge \left( {a \vee \underbrace b_1 \vee \underbrace {\neg c}_0} \right) \wedge \left( {\neg a \vee d} \right) \wedge \left( {a \vee \underbrace {\neg c}_0 \vee \neg e} \right)\]

  1. החלטה ברמה 2: נבחר plot:$a = 1$.

plot:\[\left( {\underbrace {\neg b}_0 \vee \underbrace c_1} \right) \wedge \left( {\underbrace {\neg a}_0 \vee \neg d} \right) \wedge \left( {\underbrace a_1 \vee \underbrace b_1 \vee \underbrace {\neg c}_0} \right) \wedge \left( {\underbrace {\neg a}_0 \vee d} \right) \wedge \left( {\underbrace a_1 \vee \underbrace {\neg c}_0 \vee \neg e} \right)\]

קיבלנו קונפליקט – לא קיים ערך של plot:$d$ שיספק את הנוסחה, ולכן מבצעים נסיגה.

נשים לב שבמקרה הזה זיהינו את הקונפילט באופן מיידי. לעתים הקונפילקט יתגלה רק

לאחר כמה שלבים נוספים.



  1. נסיגה: נבחר plot:$a = 0$.

plot:\[\left( {\underbrace {\neg b}_0 \vee \underbrace c_1} \right) \wedge \left( {\underbrace {\neg a}_1 \vee \neg d} \right) \wedge \left( {\underbrace a_0 \vee \underbrace b_1 \vee \underbrace {\neg c}_0} \right) \wedge \left( {\underbrace {\neg a}_1 \vee d} \right) \wedge \left( {\underbrace a_0 \vee \underbrace {\neg c}_0 \vee \neg e} \right)\]

  1. BCP: הפסוקית האחרונה מכריחה אותנו לבחור plot:$e = 0$.

plot:\[\left( {\underbrace {\neg b}_0 \vee \underbrace c_1} \right) \wedge \left( {\underbrace {\neg a}_1 \vee \neg d} \right) \wedge \left( {\underbrace a_0 \vee \underbrace b_1 \vee \underbrace {\neg c}_0} \right) \wedge \left( {\underbrace {\neg a}_1 \vee d} \right) \wedge \left( {\underbrace a_0 \vee \underbrace {\neg c}_0 \vee \underbrace {\neg e}_1} \right)\]

  1. קיבלנו השמה חלקית מספקת: plot:$a = 0,b = 1,c = 1,e = 0$. הערך של plot:$d$ יכול להיות 0 או 1.

תגיות המסמך:

לפרק הקודם6.8.1. מבוא והצגה חוזרת של הבעיה
לפרק הבא6.8.3. שיפור לאלגוריתם – יוריסטיקה לבחירת המשתנה הבא שיקבל ערך
אין תגובות!
שיתוף:
| עוד