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

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

6.8.1. מבוא והצגה חוזרת של הבעיה

בפרק זה נסטה מהדיונים על בדיקת מודל, ונרחיב על בעיית SAT, שהוצגה בקצרה בפרק הקודם.

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

השמות:

השמה מלאה נותנת ערך לכל המשתנים.
השמה חלקית נותנת ערך לחלק מהמשתנים.
השמה מספקת צריכה לספק כל אחת מהפסוקיות.

דוגמא: נביט בפסוקית הבאה: $plot:$\left( {a \vee d} \right) \wedge \left( {\neg c \vee b} \right)$$ . ההשמה היא השמה חלקית מספקת.
רוב כלי ה-SAT הקיימים מספקים השמה מלאה על ידי ריפוד השמת חלקית שנמצאת.

בעיית SAT: כאשר קיימים plot:$m$ משתנים בנוסחה קיימות $plot:${2^m}$$ השמות אפשריות שצריך לבדוק.

כאמור – ידוע פתרון אקספוננציאלי לבעיה. קיימים אלגוריתמים אותם נציג המאפשרים לפתור SAT בזמן סביר.