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

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

6.8.3. שיפור לאלגוריתם – יוריסטיקה לבחירת המשתנה הבא שיקבל ערך

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

בחירת המשתנה שמופיע הכי הרבה פעמים

לכל משתנה plot:$x$ שומרים את מספר הפסוקיות בהן הוא נמצא (באופן חיובי או שלילי). נבחר את המשתנה שהמונה שלו הגדול ביותר. (בחירה נוספת שיש לבצע – האם לתת לו ערך 0 או 1).

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

בחירת המשתנים לפי גודל הפסוקיות

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

הפסוקית הקצרה ביותר מכילה ליטרל אחד, ולכן המרחב נחצה לשניים - עבור פסוקית $plot:$\alpha = \left( x \right)$$ מתאים רק ועבור פסוקית $plot:$\beta = \left( {\neg x} \right)$$ מתאים רק . משם ממשיכים.
פסוקית בעלת 2 ליטרלים, למשל הפסוקית $plot:$\left( {x \vee y} \right)$$ , מקטינה ברבע את מרחב החיפוש, מכיוון שלא יתכן המצב $plot:$x = F \wedge y = F$$ .
ככל שהפסוקית ארוכה יותר, מרחב החיפוש מצטמצם בחלק קטן יותר (כלומר מרחב החיפוש גדול יותר).

מבחינת הביצוע, נגדיר $plot:$\delta \left( l \right) = \sum\limits_{l \in w,w \in \varphi }^{} {{2^{ - \left| w \right|}}} $$ , כאשר plot:$l$ ליטרל, plot:$w$ פסוקית, ו- $plot:$\varphi $$ נוסחת CNF.

בכל רגע נעדיף לבחור קודם את הליטרל שה- $plot:$\delta $$ שלו גדול יותר. המוטיבציה: אם ליטרל מופע בעשר פסוקיות קצרות, הוא עדיף על ליטרל שמופע ב 10 פסוקיות ארוכות. לפי ההגדרה של $plot:$\delta \left( l \right)$$ מתקיים כי ככל שהפסוקית plot:$w$ ארוכה יותר - $plot:${2^{ - \left| w \right|}}$$ קטן יותר.