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

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

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

6.5.3. BDD - דוגמא ראשונה

נתחיל להציג את נושא ה-BDD על ידי דוגמא. נתחיל בעץ החלטה בינארי ונניח שמטפלים בנוסחה plot:$\left( {a \wedge b} \right) \vee c$. סימונים: קו שלם מסמן ערך 1 למשתנה, קו מרוסק מסמן ערך 0 למשתנה.

הגרף הינו גרף מכוון ללא מעגלים (DAG – Directed Acyclic Graph).

רדוקציה ראשונה: איחוד עלים לשני מצבים - אפס ואחד.

רדוקציה שניה: איחוד תתי עצים איזומורפיים.



רדוקציה שלישית: הורדת משתנים מיותרים (שאין להם השפעה על התוצאה) למשל בדוגמה שלנו המשתנה c הימני הינו מיותר כי גם הענף הימני שלו וגם השמאלי מובילים ל- 1 ולכן אין לו השפעה על התוצאה. כך גם המשתנה b השמאלי.

לאחר הרדוקציות הנ"ל יש בידינו BDD.

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



תגיות המסמך:

לפרק הקודם6.5.2. יצוג מבנה קריפקה על ידי פונקציה בוליאנית - דוגמא
לפרק הבא6.5.4. BDD כמבנה נתונים
אין תגובות!
שיתוף:
| עוד