مخطط القرار الثنائي

في علوم الكمبيوتر ، مخطط القرار الثنائي ( BDD ) أو برنامج التفرع هو بنية بيانات تُستخدم لتمثيل دالة منطقية . وعلى مستوى أكثر تجريدًا، يمكن اعتبار مخطط القرار الثنائي تمثيلًا مضغوطًا للمجموعات أو العلاقات . وعلى عكس التمثيلات المضغوطة الأخرى، يتم إجراء العمليات مباشرة على التمثيل المضغوط، أي بدون فك الضغط.

تتضمن هياكل البيانات المماثلة الشكل الطبيعي للنفي (NNF)، ومتعددات حدود زيجالكين ، والرسوم البيانية غير الدورية الموجهة للقضايا (PDAG).

تعريف

يمكن تمثيل الدالة البوليانية على أنها رسم بياني متجذر وموجه وغير دوري ، يتكون من عدة عقد (قرار) وعقدتين طرفيتين. يتم تسمية العقدتين الطرفيتين بـ 0 (FALSE) و 1 (TRUE). يتم تسمية كل عقدة (قرار) بمتغير بولياني ولها عقدتان فرعيتان تسمىان الطفل المنخفض والطفل المرتفع. تمثل الحافة من العقدة إلى الطفل المنخفض (أو المرتفع) تعيين القيمة FALSE (أو TRUE، على التوالي) للمتغير . يسمى مثل هذا BDD "مرتبًا" إذا ظهرت متغيرات مختلفة بنفس الترتيب على جميع المسارات من الجذر. يقال إن BDD "مختصر" إذا تم تطبيق القاعدتين التاليتين على رسمه البياني:

  • دمج أي رسوم بيانية فرعية متماثلة .
  • قم بإزالة أي عقدة يكون طفليها متماثلين.

في الاستخدام الشائع، يشير مصطلح BDD دائمًا تقريبًا إلى مخطط القرار الثنائي المرتب المختزل ( ROBDD في الأدبيات، يُستخدم عندما تكون هناك حاجة إلى التأكيد على جوانب الترتيب والاختزال). تتمثل ميزة ROBDD في أنه أساسي (فريد حتى التماثل) لوظيفة معينة وترتيب متغير. [1] تجعله هذه الخاصية مفيدًا في التحقق من التكافؤ الوظيفي والعمليات الأخرى مثل تعيين التكنولوجيا الوظيفية.

يمثل المسار من العقدة الجذرية إلى الطرف الطرفي 1 تعيين متغير (ربما جزئيًا) حيث تكون الدالة المنطقية الممثلة صحيحة. عندما ينحدر المسار إلى فرع منخفض (أو مرتفع) من عقدة، يتم تعيين متغير تلك العقدة إلى 0 (أو 1 على التوالي).

مثال

يوضح الشكل الموجود على اليسار أدناه شجرة قرار ثنائية (لا يتم تطبيق قواعد الاختزال)، وجدول الحقيقة ، حيث يمثل كل منهما الدالة . في الشجرة الموجودة على اليسار، يمكن تحديد قيمة الدالة لتعيين متغير معين من خلال اتباع مسار أسفل الرسم البياني إلى طرفية. في الأشكال أدناه، تمثل الخطوط المنقطة حواف طفل منخفض، بينما تمثل الخطوط المتصلة حواف طفل مرتفع. لذلك، للعثور على ، ابدأ عند x 1 ، وانتقل لأسفل الخط المنقط إلى x 2 (نظرًا لأن x 1 له تعيين إلى 0)، ثم لأسفل خطين متصلين (نظرًا لأن x 2 وx 3 لكل منهما تعيين إلى واحد). يؤدي هذا إلى الطرفية 1، وهي قيمة .

يمكن تحويل شجرة القرار الثنائية في الشكل الأيسر إلى مخطط قرار ثنائي عن طريق تقليصها إلى الحد الأقصى وفقًا لقاعدتي التقليص. يظهر مخطط القرار الثنائي الناتج في الشكل الأيمن.

شجرة القرار الثنائية وجدول الحقيقة للوظيفة ، موصوفة في تدوين العوامل المنطقية .
BDD للدالة f

هناك طريقة أخرى لكتابة هذه الدالة المنطقية وهي .

حواف متكاملة

تمثيل مخطط القرار الثنائي باستخدام الحواف المكملة

يمكن تمثيل ROBDD بشكل أكثر إحكاما، باستخدام حواف مكملة، والمعروفة أيضًا باسم الروابط المكملة . [2] [3] يُعرف BDD الناتج أحيانًا باسم BDD المكتوب [4] أو BDD الموقع . تتشكل الحواف المكملة من خلال شرح الحواف المنخفضة على أنها مكملة أم لا. إذا كانت الحافة مكملة، فهذا يشير إلى نفي الدالة المنطقية التي تتوافق مع العقدة التي تشير إليها الحافة (الدالة المنطقية التي يمثلها BDD مع الجذر لتلك العقدة). لا يتم تكميل الحواف العالية، وذلك لضمان أن يكون تمثيل BDD الناتج شكلًا أساسيًا. في هذا التمثيل، تحتوي BDDs على عقدة ورقة واحدة، للأسباب الموضحة أدناه.

ميزتان لاستخدام الحواف المكملة عند تمثيل BDDs:

  • يستغرق حساب نفي BDD وقتًا ثابتًا
  • يتم تقليل استخدام المساحة (أي الذاكرة المطلوبة) (بعامل لا يزيد عن 2)

ومع ذلك، يزعم كنوث [5] خلاف ذلك:

على الرغم من استخدام مثل هذه الروابط من قبل جميع حزم BDD الرئيسية، فمن الصعب التوصية بها لأن برامج الكمبيوتر تصبح أكثر تعقيدًا. عادةً ما يكون توفير الذاكرة ضئيلًا، ولا يزيد أبدًا عن عامل 2؛ علاوة على ذلك، تُظهر تجارب المؤلف زيادة ضئيلة في وقت التشغيل.

إن الإشارة إلى BDD في هذا التمثيل هي "حافة" (مكملة ربما) تشير إلى جذر BDD. وهذا على النقيض من الإشارة إلى BDD في التمثيل دون استخدام حواف مكملة، والتي هي العقدة الجذرية لـ BDD. والسبب وراء ضرورة أن يكون المرجع في هذا التمثيل حافة هو أنه بالنسبة لكل دالة منطقية، يتم تمثيل الدالة ونفيها بحافة لجذر BDD وحافة مكملة لجذر نفس BDD. وهذا هو سبب استغراق النفي وقتًا ثابتًا. وهذا يفسر أيضًا سبب كفاية عقدة ورقة واحدة: يتم تمثيل FALSE بحافة مكملة تشير إلى عقدة الورقة، ويتم تمثيل TRUE بحافة عادية (أي غير مكملة) تشير إلى عقدة الورقة.

على سبيل المثال، افترض أن دالة بوليانية يتم تمثيلها باستخدام BDD يتم تمثيلها باستخدام حواف مكملة. للعثور على قيمة الدالة البوليانية لتعيين معين لقيم (بوليانية) للمتغيرات، نبدأ من الحافة المرجعية، التي تشير إلى جذر BDD، ونتبع المسار الذي تحدده قيم المتغيرات المعطاة (بمتابعة حافة منخفضة إذا كان المتغير الذي يميز العقدة يساوي FALSE، وبمتابعة الحافة المرتفعة إذا كان المتغير الذي يميز العقدة يساوي TRUE)، حتى نصل إلى العقدة الورقية. أثناء اتباع هذا المسار، نحسب عدد الحواف المكملة التي عبرناها. إذا عبرنا عند الوصول إلى العقدة الورقية عددًا فرديًا من الحواف المكملة، فإن قيمة الدالة البوليانية لتعيين المتغير المعطى تكون FALSE، وإلا (إذا عبرنا عددًا زوجيًا من الحواف المكملة)، فإن قيمة الدالة البوليانية لتعيين المتغير المعطى تكون TRUE.

يظهر على اليمين مثال لرسم تخطيطي لـ BDD في هذا التمثيل، ويمثل نفس التعبير المنطقي كما هو موضح في المخططات أعلاه، أي، . تكون الحواف المنخفضة متقطعة، والحواف العالية متصلة، والحواف المكملة يشار إليها بدائرة عند مصدرها. تمثل العقدة التي تحمل الرمز @ المرجع إلى BDD، أي أن الحافة المرجعية هي الحافة التي تبدأ من هذه العقدة.

تاريخ

الفكرة الأساسية التي تم إنشاء بنية البيانات منها هي توسعة شانون . يتم تقسيم دالة التبديل إلى دالتين فرعيتين (عوامل مساعدة) عن طريق تعيين متغير واحد (راجع الشكل الطبيعي إذا-ثم-إلا ). إذا تم اعتبار هذه الدالة الفرعية شجرة فرعية، فيمكن تمثيلها بواسطة شجرة قرار ثنائية . تم تقديم مخططات القرار الثنائية (BDDs) بواسطة CY Lee، [6] ودرسها وعرّفها Sheldon B. Akers [7] و Raymond T. Boute. [8] بشكل مستقل عن هؤلاء المؤلفين، تم تحقيق BDD تحت اسم "شكل القوس القياسي" بواسطة Yu. V. Mamrukov في CAD لتحليل الدوائر المستقلة عن السرعة. [9] تم التحقيق في الإمكانات الكاملة للخوارزميات الفعالة القائمة على بنية البيانات بواسطة Randal Bryant في جامعة كارنيجي ميلون : كانت امتداداته الرئيسية هي استخدام ترتيب متغير ثابت (للتمثيل القياسي) والرسوم البيانية الفرعية المشتركة (للضغط). يؤدي تطبيق هذين المفهومين إلى بنية بيانات فعالة وخوارزميات لتمثيل المجموعات والعلاقات. [10] [11] من خلال توسيع المشاركة إلى العديد من BDDs، أي استخدام رسم بياني فرعي واحد بواسطة العديد من BDDs، يتم تعريف بنية البيانات مخطط القرار الثنائي المخفض المشترك . [2] يُستخدم مفهوم BDD الآن بشكل عام للإشارة إلى بنية البيانات هذه.

في محاضرته المصورة " المرح مع مخططات القرار الثنائي (BDDs) ، " [12] يصف دونالد كنوث مخططات القرار الثنائي بأنها "واحدة من هياكل البيانات الأساسية الوحيدة التي ظهرت في السنوات الخمس والعشرين الماضية" ويذكر أن ورقة براينت لعام 1986 كانت لبعض الوقت واحدة من أكثر الأوراق استشهاداً في علوم الكمبيوتر.

أظهر عدنان درويش وزملاؤه أن BDDs هي واحدة من عدة أشكال طبيعية للوظائف المنطقية، وكل منها ناتج عن مجموعة مختلفة من المتطلبات. وهناك شكل طبيعي مهم آخر حدده درويش وهو الشكل الطبيعي القابل للتحلل أو DNNF.

التطبيقات

تُستخدم BDDs على نطاق واسع في برامج CAD لتجميع الدوائر ( التوليف المنطقي ) وفي التحقق الرسمي . هناك العديد من التطبيقات الأقل شهرة لـ BDD، بما في ذلك تحليل شجرة الخطأ ، والمنطق البايزي ، وتكوين المنتج، واسترجاع المعلومات الخاصة . [13] [14] [ بحاجة لمصدر ]

يمكن تنفيذ كل BDD عشوائي (حتى لو لم يتم اختزاله أو ترتيبه) مباشرة في الأجهزة عن طريق استبدال كل عقدة بمضاعف 2 إلى 1 ؛ يمكن تنفيذ كل مضاعف مباشرة بواسطة 4-LUT في FPGA . ليس من السهل التحويل من شبكة عشوائية من البوابات المنطقية إلى BDD [ بحاجة لمصدر ] (على عكس الرسم البياني العاكس و ).

تم تطبيق BDDs في مفسرين فعالين لـ Datalog . [15]

ترتيب المتغيرات

يتم تحديد حجم BDD من خلال كل من الوظيفة التي يتم تمثيلها والترتيب المختار للمتغيرات. توجد وظائف منطقية والتي بناءً على ترتيب المتغيرات سننتهي بالحصول على رسم بياني يكون عدد العقد فيه خطيًا (بالعدد  n ) في أفضل الأحوال وأسيًا في أسوأ الأحوال (على سبيل المثال، مُجمع حمل التموج ). ضع في اعتبارك الوظيفة المنطقية باستخدام ترتيب المتغيرات ، يحتاج BDD إلى عقد لتمثيل الوظيفة. باستخدام الترتيب ، يتكون BDD من عقد.

BDD للدالة ƒ ( x 1 , ..., x 8 ) = x 1 x 2 + x 3 x 4 + x 5 x 6 + x 7 x 8 باستخدام ترتيب متغير سيئ
ترتيب متغير جيد

من الأهمية بمكان الاهتمام بترتيب المتغيرات عند تطبيق بنية البيانات هذه عمليًا. مشكلة إيجاد أفضل ترتيب للمتغيرات صعبة للغاية . [16] بالنسبة لأي ثابت c  > 1، من الصعب للغاية حساب ترتيب متغير ينتج عنه OBDD بحجم أكبر من الحجم الأمثل بـ c مرات على الأكثر. [17] ومع ذلك، توجد طرق استدلالية فعالة لمعالجة المشكلة. [18]

توجد دوال يكون حجم الرسم البياني فيها دائمًا أسيًا - بغض النظر عن ترتيب المتغيرات. ينطبق هذا على سبيل المثال على دالة الضرب. [1] في الواقع، لا تحتوي الدالة التي تحسب البت الأوسط من حاصل ضرب عددين من البتات على OBDD أصغر من الرؤوس. [19] (إذا كانت دالة الضرب تحتوي على OBDD بحجم متعدد الحدود، فسيُظهر ذلك أن تحليل العوامل الصحيحة يكون في P/poly ، وهو أمر غير معروف أنه صحيح. [20] )

اقترح الباحثون تحسينات على بنية بيانات BDD مما أفسحت المجال لعدد من الرسوم البيانية ذات الصلة، مثل BMD ( مخططات اللحظة الثنائية )، وZDD ( مخططات القرار المكبوتة صفرًا )، وFBDD (مخططات القرار الثنائية المجانية)، وFDD (مخططات القرار الوظيفية)، وPDD (مخططات قرار التكافؤ)، وMTBDDs (BDDs الطرفية المتعددة).

العمليات المنطقية على أجهزة BDD

يمكن تنفيذ العديد من العمليات المنطقية على BDDs من خلال خوارزميات معالجة الرسم البياني في الوقت متعدد الحدود : [21] : 20 

ومع ذلك، فإن تكرار هذه العمليات عدة مرات، على سبيل المثال تكوين اقتران أو فصل مجموعة من BDDs، قد يؤدي في أسوأ الأحوال إلى BDD كبير بشكل كبير. وذلك لأن أيًا من العمليات السابقة لـ BDDين قد يؤدي إلى BDD بحجم متناسب مع حاصل ضرب أحجام BDDs، وبالتالي بالنسبة للعديد من BDDs، قد يكون الحجم أسيًا في عدد العمليات. يجب النظر في ترتيب المتغيرات من جديد؛ ما قد يكون ترتيبًا جيدًا لـ (بعض) مجموعة BDDs قد لا يكون ترتيبًا جيدًا لنتيجة العملية. أيضًا، نظرًا لأن إنشاء BDD لدالة بوليانية يحل مشكلة قابلية إرضاء البوليانية الكاملة NP ومشكلة التكرار الكامل co-NP ، فإن إنشاء BDD يمكن أن يستغرق وقتًا أسيًا في حجم الصيغة البوليانية حتى عندما يكون BDD الناتج صغيرًا.

إن حساب التجريد الوجودي على متغيرات متعددة من BDDs المخفضة هو NP-كامل. [22]

يمكن إجراء عد النماذج، وهو عد عدد المهام التي تحقق الغرض من صيغة بوليانية، في وقت متعدد الحدود بالنسبة لـ BDDs. بالنسبة للصيغ القياسية العامة، تكون المشكلة ♯P -complete وتتطلب أفضل الخوارزميات المعروفة وقتًا أسيًا في أسوأ الحالات.

انظر أيضا

مراجع

  1. ^ ab Bryant, Randal E. (أغسطس 1986). "Graph-Based Algorithms for Boolean Function Manipulation" (PDF) . IEEE Transactions on Computers . C-35 (8): 677–691. CiteSeerX  10.1.1.476.2952 . doi :10.1109/TC.1986.1676819. S2CID  10385726.
  2. ^ ab Brace, Karl S.; Rudell, Richard L.; Bryant, Randal E. (1990). "Efficient Implementation of a BDD Package". Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC 1990) . IEEE Computer Society Press. ص. 40–45. doi :10.1145/123186.123222. ISBN 978-0-89791-363-8.
  3. ^ Somenzi, Fabio (1999). "Binary decision diagrams" (PDF) . Calculational system design . NATO Science Series F: Computer and systems sciences. المجلد 173. IOS Press. ص 303-366. ISBN 978-90-5199-459-9.
  4. ^ جان كريستوف مادري؛ جان بول بيلون. "إثبات صحة الدائرة باستخدام مقارنة رسمية بين السلوك المتوقع والمستخرج". وقائع المؤتمر الخامس والعشرين لجمعية الحوسبة الآلية ومعهد مهندسي الكهرباء والإلكترونيات حول أتمتة التصميم، DAC '88، أناهايم، كاليفورنيا، الولايات المتحدة الأمريكية، 12-15 يونيو 1988. doi : 10.1109/DAC.1988.14759.
  5. ^ Knuth, DE (2009). Fascicle 1: Bitwise tricks & techniques; Binary Decision Diagrams . The Art of Computer Programming . المجلد 4. Addison–Wesley. ISBN 978-0-321-58050-4.مسودة المجلد 1ب مؤرشفة بتاريخ 12 مارس 2016 على موقع Wayback Machine ومتاحة للتنزيل
  6. ^ Lee, CY (1959). "تمثيل دوائر التبديل بواسطة برامج القرار الثنائي". مجلة Bell System Technical Journal . 38 (4): 985–999. doi :10.1002/j.1538-7305.1959.tb01585.x.
  7. ^ Akers, Jr., Sheldon B (June 1978). "Binary Decision Diagrams". IEEE Transactions on Computers . C-27 (6): 509–516. doi :10.1109/TC.1978.1675141. S2CID  21028055.
  8. ^ بوت، رايموند ت. (يناير 1976). "آلة القرار الثنائي كجهاز تحكم قابل للبرمجة". نشرة يوروميكرو . 1 (2): 16-22. doi :10.1016/0303-1268(76)90033-X.
  9. ^ مامروكوف، يو. ف. (1984). تحليل الدوائر غير الدورية والعمليات غير المتزامنة (دكتوراه). معهد لينينغراد الكهروتقني.
  10. ^ براينت، راندال إي. (1986). "خوارزميات تعتمد على الرسوم البيانية لمعالجة الدالة المنطقية" (PDF) . معاملات معهد مهندسي الكهرباء والإلكترونيات على الحاسبات . C-35 (8): 677–691. doi :10.1109/TC.1986.1676819. S2CID  10385726.
  11. ^ براينت، راندال إي. (سبتمبر 1992). "التلاعب الرمزي بالبيانات المنطقية باستخدام مخططات القرار الثنائية المرتبة". استطلاعات الحوسبة التابعة لـ ACM . 24 (3): 293–318. doi :10.1145/136035.136043. S2CID  1933530.
  12. ^ "مركز ستانفورد للتنمية المهنية". scpd.stanford.edu . مؤرشف من الأصل في 2014-06-04 . تم الاسترجاع في 2018-04-23 .
  13. ^ Jensen, RM (2004). "CLab: A C++ library for fast backtrack-free interactive product configuration". وقائع المؤتمر الدولي العاشر حول مبادئ وممارسة برمجة القيود . محاضرات في علوم الكمبيوتر. المجلد 3258. Springer. ص 816. doi :10.1007/978-3-540-30201-8_94. ISBN 978-3-540-30201-8.
  14. ^ Lipmaa, HL (2009). "First CPIR Protocol with Data-Dependent Computation" (PDF) . المؤتمر الدولي حول أمن المعلومات والتشفير . محاضرات في علوم الكمبيوتر. المجلد 5984. Springer. ص 193-210. doi :10.1007/978-3-642-14423-3_14. ISBN 978-3-642-14423-3.
  15. ^ Whaley, John; Avots, Dzintars; Carbin, Michael; Lam, Monica S. (2005). "استخدام سجل البيانات مع مخططات القرار الثنائية لتحليل البرامج". في Yi, Kwangkeun (محرر). لغات البرمجة والأنظمة . مذكرات محاضرات في علوم الكمبيوتر. المجلد 3780. برلين، هايدلبرغ: سبرينغر. ص 97-118. doi :10.1007/11575467_8. ISBN 978-3-540-32247-4. S2CID  5223577.
  16. ^ بوليج، بيات؛ ويجنر، إنجو (سبتمبر 1996). "تحسين ترتيب المتغيرات في أجهزة OBDD هو NP-Complete". معاملات معهد مهندسي الكهرباء والإلكترونيات على الحاسبات . 45 (9): 993-1002. doi :10.1109/12.537122.
  17. ^ سيلينج، ديتليف (2002). "عدم إمكانية تقريب تقليل OBDD". المعلومات والحوسبة . 172 (2): 103-138. doi : 10.1006/inco.2001.3076 .
  18. ^ رايس، مايكل. "دراسة استقصائية لأساليب ترتيب المتغيرات الثابتة لبناء BDD/MDD بكفاءة" (PDF) .
  19. ^ Woelfel, Philipp (2005). "حدود حجم OBDD لضرب الأعداد الصحيحة عبر التجزئة الشاملة". مجلة علوم الحاسب والنظام . 71 (4): 520-534. CiteSeerX 10.1.1.138.6771 . doi : 10.1016/j.jcss.2005.05.004 . 
  20. ^ ريتشارد جيه ليبتون . "BDD's and Factoring". رسالة جودل المفقودة وP=NP ، 2009.
  21. ^ أندرسن، إتش آر (1999). "مقدمة إلى مخططات القرار الثنائي" (PDF) . ملاحظات المحاضرة . جامعة كوبنهاجن لتكنولوجيا المعلومات.
  22. ^ هوث، مايكل؛ ريان، مارك (2004). المنطق في علوم الكمبيوتر: النمذجة والاستدلال حول الأنظمة (الطبعة الثانية). مطبعة جامعة كامبريدج. ص 380-. ISBN 978-0-52154310-1. OCLC  54960031.

قراءة إضافية

  • أوبار، ر. (1976). "إنشاء اختبار للدوائر الرقمية باستخدام الرسوم البيانية البديلة". وقائع جامعة تالين التقنية (بالروسية) (409). تالين، إستونيا: 75-81.
  • Meinel, C.; Theobald, T. (2012) [1998]. Algorithms and Data Structures in VLSI-Design: OBDD – Foundations and Applications (PDF) . Springer. ISBN 978-3-642-58940-9.الكتاب الكامل متاح للتحميل.
  • إبندت، روديجر. فاي، جورشوين؛ دريشسلر، رولف (2005). تحسين BDD المتقدم . سبرينغر. رقم ISBN 978-0-387-25453-1.
  • بيكر، بيرند. دريشسلر، رولف (1998). مخططات القرار الثنائي: النظرية والتنفيذ . سبرينغر. رقم ISBN 978-1-4419-5047-5.
  • المتعة مع مخططات القرار الثنائي (BDDs)، محاضرة لدونالد كنوث
  • قائمة مكتبات برامج BDD للعديد من لغات البرمجة.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Binary_decision_diagram&oldid=1253922024"
Original text
Rate this translation
Your feedback will be used to help improve Google Translate