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

בהינתן שני BDD: plot:$f,f'$ נרצה לחשב את ה-BDD של plot:$f \circ f'$ כאשר plot:$ \circ $ הוא אחת מ-16 הפונקציות הבינאריות. סימונים: plot:$v,v'$ הם השורשים של plot:$f,f'$ בהתאמה. אם 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'$):

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

    וה-BDD הוא גם צומת יחיד plot:$v''$ כך שמתקיים plot:$value\left( {v''} \right) = value\left( v \right) \circ
      value\left( {v'} \right)$
  2. אם 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:$v''$ כך שיתקיים:
    1. plot:$low\left( {v''} \right)$ יצביע אל ה-BDD:plot:$f{|_{x = 0}} \circ f'{|_{x = 0}}$
    2. plot:$high\left( {v''} \right)$ יצביע אל ה-BDD: plot:$f{|_{x = 1}} \circ f'{|_{x = 1}}$.

דוגמא:

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

ואחרי צמצום:



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

  1. באופן דומה ל-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|$.

אין תגובות!
שיתוף:
| עוד