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

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

6.5.5.3. פעולות בוליאניות על BDD (Apply)

בהינתן שני BDD: plot:$f,f'$ נרצה לחשב את ה-BDD של $plot:$f \circ f'$$ כאשר $plot:$ \circ $$ הוא אחת מ-16 הפונקציות הבינאריות. סימונים: plot:$v,v'$ הם השורשים של בהתאמה. אם אינם צמתי קצה אז $plot:$\operatorname{var} \left( v \right) = x$$ וכן $plot:$\operatorname{var} \left( {v'} \right) = x'$$ .

נסתמך על "הרחבת Shonon": $plot:$f = \left( {\neg x \wedge f{|_{x = 0}}} \right) \vee \left( {x \wedge {f_{|x = 1}}} \right)$$

Apply עובדת לפי ארבעה מקרים שונים: (חישוב $plot:$f \circ f'$$ ):

אם הם צמתי קצה אז תוצאת הפעולה היא $plot:$f \circ f' = value\left( v \right) \circ value\left( {v'} \right)$$

וה-BDD הוא גם צומת יחיד כך שמתקיים $plot:$value\left( {v''} \right) = value\left( v \right) \circ value\left( {v'} \right)$$
אם $plot:$\operatorname{var} \left( v \right) = \operatorname{var} \left( {v'} \right) = x$$ אז $plot:\[f \circ f' = \left( {\neg x \wedge \left( {f{|_{x = 0}} \circ f'{|_{x = 0}}} \right)} \right) \vee \left( {x \wedge \left( {f{|_{x = 1}} \circ f'{|_{x = 1}}} \right)} \right)\]$ .

בניית ה-BDD: צומת חדש עם משתנה כך שיתקיים:

$plot:$low\left( {v''} \right)$$ יצביע אל ה-BDD: $plot:$f{|_{x = 0}} \circ f'{|_{x = 0}}$$
$plot:$high\left( {v''} \right)$$ יצביע אל ה-BDD: $plot:$f{|_{x = 1}} \circ f'{|_{x = 1}}$$ .

דוגמא:

נחשב את $plot:$f \vee f'$$ :

ואחרי צמצום:

אם $plot:$x = \operatorname{var} \left( v \right) < \operatorname{var} \left( {v'} \right)$$ כאשר היחס מוגדר על סדר נתון, (כלומר $plot:$\operatorname{var} \left( v \right)$$ לא מופיע ב או בניסוח אחר: $plot:$f' = f'{|_{x = 0}} = f'{|_{x = 1}}$$ ) אז:

$plot:$f \circ f' = \left( {\neg x \wedge \left( {f{|_{x = 0}} \circ f'} \right)} \right) \vee \left( {x \wedge \left( {f{|_{x = 1}} \circ f'} \right)} \right)$$

באופן דומה ל-3 נטפל במצב בו $plot:$x = \operatorname{var} \left( v \right) > \operatorname{var} \left( {v'} \right)$$ .

דוגמא

יהיו 2 פונקציות plot:$f,f'$ מעל המשתנים plot:$a,b$ . נקבע את סדר המשתנים להיות plot:$a
< b$ .

הפונקציות עצמן הינן:

$plot:$\begin{gathered} f:a \to b \hfill \\ f':\neg b \hfill \\ \end{gathered} $$

נרצה לחשב את הפונקציה $plot:$f \leftrightarrow f'$$ . המקרה כאן הוא מקרה 3.

ומכאן נקבל:

אנו מקבלים כי:

$plot:$\left( {a \to b} \right) \leftrightarrow \neg b = \neg a \wedge \neg b$$

ניתן להגיע לאותו הפיתוח באמצעות שימוש בלוגיקה, לבדיקה:

$plot:$f \leftrightarrow f' \equiv \left( {a \to b} \right) \leftrightarrow \neg b \equiv \left( {\neg a \vee b} \right) \leftrightarrow \neg b \equiv \neg a \wedge \neg b$$

סיבוכיות פעולה APPLY

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

ב-BDD.

נשתמש בטבלת HASH: לכל הפעלה של APPLY יש מצביעים לצמתים ב-BDD שמהם הפעולה הופעלה, וכן את הפעולה שהופעלה. לא נבצע את אותו חישוב פעמיים אלא נשתמש בתוצאות שכבר חישבנו.

כעת הסיבוכיות תלויה בכמות פעולות ה-APPLY השונות שמבצעים במהלך תהליך APPLY על $plot:$f \circ f'$$ . נסמן ב- $plot:$\left| f \right|$$ את מספר הצמתים ב-BDD של plot:$f$ ומכאן: מספר הפעולות הוא $plot:$\left| f \right| \cdot \left| {f'} \right|$$ .