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

6.8.4. שיפור לאלגוריתם – שימוש במבנה נתונים חכם לזרוז BCP

מוטיבציה: זמן ניכר מריצת ה-SAT Solver (יכול להגיע אף ל-90% מהזמן) עסוק האלגוריתם בביצוע BCP. כדי לשפר את מהירות הפעולה נרצה לשפר את ביצוע BCP, כלומר – זיהוי מהיר של פסוקיות יחידה.

הרעיון:

• לכל משתנה תהיה הצבעה ממנו אל כל הפסוקיות שבהן הוא מופיע (חיובי או שלילי).
• לכל פסוקית יהיו שני מצביעים ("שומרים") המצביעים ל-2 ליטרלים שאין להם ערך בהשמה.
• הרעיון: בפסוקית יש הרבה ליטרלים. כל זמן שיש 2 ליטרלים שאין להם השמה – אנו יודעים כי הפסוקית עדיין אינה פסוקית יחידה.

ביצוע:

• בהחלטה או ב-BCP, כאשר משתנה קיבל ערך, לכל פסוקית ש- משתתף בה (אופציונלי: ושאינה ספיקה), נבצע את הפעולות הבאות:
• אם הפסוקית כבר ספיקה – לא עושים כלום (עוצרים).
• אם הוא איננו אחד מהשומרים – לא עושים כלום (עוצרים).
• אם הוא שומר והליטרל שבו הוא מופיע קיבל ערך true מסמנים את הפסוקית כספיקה ועוצרים.
• אם הוא שומר והליטרל הוא false, מחפשים בפסוקית ליטרל חדש שאינו שומר ושאין לו ערך.
• אם יש כזה – הליטרל החדש הופך לשומר.
• אם אין כזה – זוהי פסוקית יחידה. מציבים ערך true לשמור השני.