דיאגרמת החלטה בינארית

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

הגדרה
BDD הוא גרף מכוון חסר מעגלים בעל צומת מקור בודד, ובו דרגת היציאה של כל הצמתים היא 2, למעט שני צמתי בור (עלים) המסומנים בתוויות 0 (שקר) ו-1 (אמת). הצמתים שאינם צמתי בור מכונים צמתי החלטה, ולכל אחד מהם מוצמדת תווית עם משתנה בוליאני . שתי הקשתות היוצאות מכל צומת החלטה מסומנות אף הן בתוויות: לאחת ניתנת התווית 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.

דוגמה
נתונה הפונקציה הבוליאנית . התרשים הימני מציג את טבלת האמת של  וכן עץ החלטה בינארי עבור הפונקציה. הקשתות המקווקוות הן קשתות עם התוויות low, ולקשתות המלאות תווית high. ניתן לראות שבעץ ההחלטה קיימים תתי עצים איזומורפים המהווים יתירות. התרשים השמאלי מציג ROBDD עבור , בו הופעלו כללי הצמצום, ועל כן אין בו תתי גרפים איזומורפים.
 ממוזער|546px|טבלת אמת ועץ החלטה בינארי עבור הפונקציה  ממוזער|189px|ROBDD עבור הפונקציה 

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

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

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

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

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

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

BDD כמבנה נתונים הוצג לראשונה על ידי לי (C. Y. Lee) ב-1958 תחת השם Binary-Decision Programs. לי ניצל את השיטה של שאנון כדי ליצור מבנה נתונים שהוא שלב ביניים בין הדרישות הלוגיות לבין המעגל החשמלי שמממש אותן. את השם BDD קבע אקרז (Akerz) במאמר מ-1978. באופן בלתי תלוי, מעבר למסך הברזל, פיתח ממרוקוב (Yu. V. Mamrukov) מבנה נתונים דומה, ונתן לו את השם Canonical Bracket Form.

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

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

מבני נתונים דומים
עבור שימושים שונים, פותחו מספר מבני נתונים שמכלילים BDD או משפרים אותו. להלן כמה דוגמאות:
 Signed BDD - לקשתות עם תווית low מוסיפים ביט המציין האם הן מצביעות על הפונקציה המיוצגת על ידי צומת היעד או על שלילתה. תוספת זו מאפשרת ביצוע שלילה של פונקציה בזמן , וכן ייצוג יותר קומפקטי בזיכרון (עד פי 2), זאת על חשבון זמן הביצוע של פעולות אחרות. ידוע גם בשמות complemented edges, complement links ו-typed BDD.
 ZDD (Zero-suppressed BDD) - מתקבל על ידי הפעלה של חוק צמצום שונה: מותר ששתי הקשתות היוצאות מצומת נתון יובילו לאותו צומת, אך אסור שקשת עם תווית high תוביל לצומת הבור 0. מאפשר יצוג יותר קומפקטי של קבוצות דלילות של וקטורים בינאריים.
 MTBDD (Multi Terminal BDD) - מאפשר צמתי בור מקבוצה סופית כלשהי; לאו דווקא הקבוצה . בכך מתאפשר יצוג של פונקציות עם תחום בינארי וטווח סופי נתון.

קישורים חיצוניים

 הערות שוליים 

קטגוריה:אלגברה בוליאנית
קטגוריה:מבני נתונים