משתמש: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

פעולות לוגיות

שימושים

היסטוריה

צמתי החלטה ב-BDD מממשים למעשה זהות שנוסחה לראשונה על ידי ג'ורג' בול ב-1854,^[1] ולפיה ניתן לפרק כל פונקציה בוליאנית לשתי תתי פונקציות בהנתן אחד מהמשתנים: האחת מתקבלת מהצבת הערך 0 למשתנה, והשניה מהצבת הערך 1. בצורה פורמלית: $F=x\cdot F_{x}+x'\cdot F_{x'}$ , כאשר $x$ הוא המשתנה הנבחר, $x'$ היא שלילתו, $F_{x}$ היא הפונקציה המתקבלת מ- $F$ על ידי ההצבה $x=1$ , ו- $F_{x'}$ היא הפונקציה המתקבלת על ידי ההצבה $x=0$ .

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

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

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

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

מבני נתונים דומים

הערות שוליים

^ George Boole, Investigation of the Laws of Thought: On which are Founded the Mathematical Theories of Logic and Probabilities, 1854, עמ' 72
^ Claude Shannon, The Synthesis of Two-Terminal Switching Circuits, Bell System Technical Journal 28, 1949, עמ' 59–98
^ Lee, C.Y., Representation of Switching Circuits by Binary-Decision Programs, Bell System Technical Journal 38(4), 1959, עמ' 985-999
^ Mamrukov, Yu. V., Analysis of aperiodic circuits and asynchronous processes, PhD Thesis, Leningrad Electrotechnical Institute, 1984
^ Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers C-35, 1986, עמ' 677–691
^ Bryant, Randy (Randal E.) oral history, Computer History Museum
^ Fun With Binary Decision Diagrams (BDDs), Computer Musings by Professor Donald E. Knuth

[1] George Boole, Investigation of the Laws of Thought: On which are Founded the Mathematical Theories of Logic and Probabilities, 1854, עמ' 72

[2] Claude Shannon, The Synthesis of Two-Terminal Switching Circuits, Bell System Technical Journal 28, 1949, עמ' 59–98

[3] Lee, C.Y., Representation of Switching Circuits by Binary-Decision Programs, Bell System Technical Journal 38(4), 1959, עמ' 985-999

[4] Mamrukov, Yu. V., Analysis of aperiodic circuits and asynchronous processes, PhD Thesis, Leningrad Electrotechnical Institute, 1984

[5] Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers C-35, 1986, עמ' 677–691

[6] Bryant, Randy (Randal E.) oral history, Computer History Museum

[7] Fun With Binary Decision Diagrams (BDDs), Computer Musings by Professor Donald E. Knuth

[1]

[2]

[3]

[4]

[5]

[6]

[7]