הועלה לאתר:  
מספר עמודים: 120
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

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

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

6.5.5.1. פעולת צמצום – (Reduce)

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

  • ביטול צמתי קצה כפולים:

    נשאיר צומת קצה בודד עם ערך 0 ואחד עם ערך 1, ונפנה את כל ההצבעות בהתאם.
  • ביטול צמתים פנימיים כפולים:

    בהינתן צמתיםplot:$u,v$ כך שמתקיים

plot:$\operatorname{var} \left( v \right) = \operatorname{var} \left( u \right),high\left( v \right) = high\left( u \right),low\left( v \right) = low\left( u \right)$

אזי מבטלים את אחד הצמתים ומפנים את כל ההצבעות שהיו אליו אל הצומת שנשאר.

  • ביטול צמתים מיותרים plot:$low\left( v \right) = high\left( v \right)$

    נבטל את הצומת v ונפנה ההצבעות אליו אל הבן היחיד שלו.

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

אלגוריתם reduce: עובד מהעלים כלפי מעלה ומצמצם את ה-BDD בזמן שהוא ליניארי בגודל ה-BDD.



תגיות המסמך:

לפרק הקודם6.5.5. פעולות על BDDs:
לפרק הבא6.5.5.2. פעולת הגבלה - restriction
אין תגובות!
שיתוף:
| עוד