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

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

6.5.4. BDD כמבנה נתונים

BDD עבור פונקציה בוליאנית $plot:$f\left( {{x_1}...{x_n}} \right)$$ הינו גרף מכוון חסר מעגלים עם שורש ושני סוגי צמתים: צמתי קצה וצמתים פנימיים. שורש העץ יכול להיות צומת קצה או צומת פנימי.

לצומת פנימי plot:$v$ יש את השדות הבאים:

משתנה $plot:$\operatorname{var} \left( v \right)$$
שני מצביעים: $plot:$low\left( v \right),high\left( v \right)$$ .

לצומת קצה יש ערך בודד: $plot:$value\left( v \right) \in \left\{ {0,1} \right\}$$

על מנת להבטיח יצוג קנוני נוסיף את התנאים הבאים:

כל משתנה מופיע פעם אחת לכל היותר על כל מסלול מהשורש לעלה.
נגדיר סדר למשתנים. המשתנים מופיעים באותו סדר לאורך כל מסלול מהשורש לעלה (לא בהכרח כולם מופיעים). מוסכמה – הסדר הינו סדר עולה מהשורש לעלים.
הגרף אינו מכיל תתי גרפים איזומורפיים או צמתים מיותרים (שאין תלות בערך המשתנה בהם על המסלול המסוים).

עם מגבלות אלו מתקבל Reduced Ordered BDD (ROBDD). בהמשך, כאשר נדבר על BDD נתכוון תמיד ל-ROBDD.

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

בהינתן BDD – איזו פונקציה הוא מגדיר:

בהינתן BDD עם שורש plot:$v$ הוא מגדיר פונקציה $plot:${f_v}\left( {{x_1},...{x_n}} \right)$$ באופן הבא:

אם צומת קצה - $plot:\[{f_v}\left( {{x_1}...{x_n}} \right) = value\left( v \right)\]$
אם אינו צומת קצה ואם $plot:$var\left( v \right) = {x_i}$$ אזי:

$plot:${f_v}\left( {{x_1}...{x_n}} \right) = \left( {\neg {x_i} \wedge {f_{low\left( v \right)}}\left( {{x_1}...{x_n}} \right)} \right) \vee \left( {{x_i} \wedge {f_{high\left( v \right)}}\left( {{x_1}...{x_n}} \right)} \right)$$

נמשיך עם שרטוט הדוגמא:

נחשב את $plot:${f_v}$$ עבור ה-BDD:

מתקיים: $plot:$\operatorname{var} \left( {{v_1}} \right) = a,\operatorname{var} \left( {{v_2}} \right) = b,\operatorname{var} \left( {{v_3}} \right) = c$$ וכמו כן $plot:$value\left( {{v_4}} \right) = 0,value\left( {{v_5}} \right) = 1$$ .

$plot:${f_{{v_4}}}\left( {a,b,c} \right) = 0$$

$plot:${f_{{v_5}}}\left( {a,b,c} \right) = 1$$

$plot:${f_{{v_3}}}\left( {a,b,c} \right) = \left( {\neg c \wedge {f_{{v_4}}}\left( {a,b,c} \right)} \right) \vee \left( {c \wedge {f_{{v_5}}}\left( {a,b,c} \right)} \right) = \left( {\neg c \wedge 0} \right) \vee \left( {c \wedge 1} \right) = c$$

$plot:${f_{{v_2}}}\left( {a,b,c} \right) = \left( {\neg b \wedge c} \right) \vee \left( {b \wedge 1} \right) = b \vee c$$

$plot:\[{f_{{v_1}}}\left( {a,b,c} \right) = \left( {\neg a \wedge c} \right) \vee \left( {a \wedge \left( {b \vee c} \right)} \right) = \left( {a \wedge b} \right) \vee c\]$

עובדות על BDD:

כל צומת ב-BDD מייצג איזשהו "זכרון".
לא לכל פונקציה בוליאנית קיים BDD "קטן" פולינומיאלית במספר משתני הפונקציה. יש $plot:${2^{{2^n}}}$$ פונקציות בוליאניות עם משתנים, ויש הרבה פחות DAG בגודל פולינומיאלי ב-.
לפונקצית הכופל אין BDD פולינומיאלי לכל סדר שהוא.

פונקצית הכופל היא הפונקציה המקבלת שני מספרים ביצוג בינארי: $plot:${b_1}....{b_n},{a_1}...{a_n}$$ ומחזירה את המכפלה שלהם ביצוג $plot:${c_1}...{c_{2n}}$$ .
מציאת הסדר האופטימלי של המשתנים ב-BDD היא בעיית NP-קשה.