משתמש:Zivn/דיאגרמת החלטה בינארית

דיאגרמת החלטה בינארית (באנגלית: Binary Decision Diagram או בקיצור BDD) היא מבנה נתונים לייצוג קומפקטי של פונקציות בינאריות. ניתן לייצג באמצעות מבנה נתונים זה גם קבוצות ויחסים, תוך שימוש בפונקציה המציינת שלהם, וכן לבצע ביעילות יחסית פעולות כגון חיתוך, איחוד, משלים וכימות, ושאילתות כגון שייכות, הכלה וזהות. השימוש ב-BDD נפוץ בעיקר בתכנון מעגלים משולבים, באימות שבבים ובאימות תוכנה.

הגדרה

BDD הוא גרף מכוון חסר מעגלים בעל צומת מקור בודד, ובו דרגת היציאה של כל הצמתים היא 2, למעט שני צמתי בור (עלים) המסומנים בתוויות 0 (שקר) ו-1 (אמת). הצמתים שאינם צמתי בור מכונים צמתי החלטה, ולכל אחד מהם מוצמדת תווית עם משתנה בוליאני $x_{i}$. שתי הקשתות היוצאות מכל צומת החלטה מסומנות אף הן בתוויות: לאחת ניתנת התווית low, ולשניה התווית high. הקשת המסומנת בתווית low מייצגת השמה של הערך 0 למשתנה הבוליאני בו סומן הצומת ממנו יצאה הקשת. הקשת המסומנת בתווית high מייצגת השמה של הערך 1 לאותו משתנה.

כל BDD מייצג פונקציה בוליאנית יחידה. כדי לחשב את ערך הפונקציה על הצבה נתונה למשתנים הבוליאנים, יש להתחיל מצומת המקור, ולבחון את הערך שקיבל בהצבה המשתנה בתווית של צומת זה. אם הערך הוא 0, יש לעבור לצומת המוצבע על ידי הקשת עם התווית low. אם הערך הוא 1, יש לעבור לצומת המוצבע על ידי הקשת עם התווית high. בצומת הבא, יש לבחון שוב את הערך שקיבל בהצבה המשתנה של הצומת (יתכן שכעת זהו משתנה אחר). בהתאם לערך, יש לבחור את קשת היציאה ולהמשיך לצומת הבא. כך יש להמשיך עד שמגיעים לאחד מצמתי הבור. ערך הפונקציה על ההצבה נתון על ידי התווית של צומת הבור.

BDD יקרא סדור (ordered) אם על תוויות הצמתים בכל מסלול מצומת המקור לאחד מצמתי הבור מופיעים המשתנים הבוליאניים לפי סדר נתון.

BDD יקרא מצומצם (reduced) אם מתקיימים בו שני הכללים הבאים:

• אין בגרף שני תתי גרף איזומורפים.
• אין בגרף צומת ששתי הקשתות היוצאות ממנו מצביעות לאותו צומת.

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

ב-ROBDD, כל מסלול מצומת המקור לצומת הבור עם התווית 1, מייצג הצבה (יתכן חלקית) עליה הפונקציה מחזירה 1. אם עוברים דרך קשת עם התווית low, המשתנה בצומת ממנה יצאה הקשת מקבל את הערך 0. עם עוברים דרך קשת עם התווית high המשתנה מקבל את הערך 1.

דוגמה

נתונה הפונקציה הבוליאנית $f(x_{1},x_{2},x_{3})=(\neg x_{1}\wedge \neg x_{2}\wedge \neg x_{3})\vee (x_{1}\wedge x_{2})\vee (x_{2}\wedge x_{3})$. התרשים הימני מציג את טבלת האמת של $f$ וכן עץ החלטה בינארי עבור הפונקציה. הקשתות המקווקוות הן קשתות עם התוויות low, ולקשתות המלאות תווית high. ניתן לראות שבעץ ההחלטה קיימים תתי עצים איזומורפים המהווים יתירות. התרשים השמאלי מציג ROBDD עבור $f$, בו הופעלו כללי הצמצום, ועל כן אין בו תתי גרפים איזומורפים.

טבלת אמת ועץ החלטה בינארי עבור הפונקציה $f$

ROBDD עבור הפונקציה $f$

היסטוריה

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

בסדרת ההרצאות המפורסמת Computer Musings, הקדיש דונלד קנות' ב-2008 הרצאה שלמה ל-BDD וגרס כי זהו מבנה הנתונים היסודי היחיד שהומצא בעשרים וחמש השנים האחרונות.