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

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

6.7.1. תזכורת – בעיית SAT

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

קיימים בשוק פותרי SAT (SAT Solvers) המקבלים נוסחה פסוקית ומחזירים אם היא ספיקה או לא. רובם מבוססים על נוסחאות במבנה CNF.

מושגים:

משתנה בוליאני: משתנה שיכול לקבל 0 או 1.
ליטרל: $plot:$x,\neg x$$ (משתנה בוליאני או שלילה שלו)
פסוקית: $plot:$\left( {{x_1} \vee {x_2} \vee \neg {x_3}} \right)$$ (רשימה של ליטרלים עם סימן $plot:$ \vee $$ ביניהם)
פסוק CNF: $plot:$\left( {{x_1} \vee {x_2} \vee \neg {x_3}} \right) \wedge \left( {... \vee ... \vee } \right) \wedge \left( {} \right)...$$ (רשימה של פסוקיות עם $plot:$ \wedge $$ ביניהן). חשוב לדעת: ניתן לתרגם כל פסוק לפסוק מקביל במבנה CNF.

השמה:

השמה נותנת ערכים למשתנים של הנוסחה - T או F, (1 או 0).
דוגמה להשמה: $plot:$A = \left\{ {{x_1} = 0,{x_2} = 1,{x_3} = 0,...} \right\}$$
השמה מלאה נותנת ערך לכל המשתנים.
השמה חלקית נותנת ערך לחלק מהמשתנים. למשל: $plot:$A = \left\{ {{x_7} = 0,{x_2} = 0} \right\}$$ .