خوارزمية DPLL

📅 آخر تحديث: ١٨ يوليو ٢٠٢٦
✍️ نُشر في: ١٨ يوليو ٢٠٢٦
📷 يحتوي على 28 صور
الموسوعة الحرة

في المنطق وعلوم الحاسوب ، تعتبر خوارزمية ديفيس-بوتنام-لوجمان-لوفلاند ( DPLL ) خوارزمية بحث كاملة تعتمد على التراجع لتحديد مدى إمكانية إرضاء صيغ المنطق الافتراضي في الشكل الطبيعي الاقتراني ، أي لحل مشكلة CNF-SAT .

طُرحت هذه الخوارزمية عام 1961 على يد مارتن ديفيس وجورج لوغيمان ودونالد دبليو لوفلاند ، وهي تطوير لخوارزمية ديفيس-بوتنام السابقة ، وهي إجراء قائم على التحليل طوّره ديفيس وهيلاري بوتنام عام 1960. في المنشورات القديمة تحديدًا، يُشار إلى خوارزمية ديفيس-لوغيمان-لوفلاند غالبًا باسم "طريقة ديفيس-بوتنام" أو "خوارزمية ديفيس-بوتنام". ومن الأسماء الشائعة الأخرى التي تحافظ على التمييز بينهما: DLL وDPLL.

التطبيقات والتنفيذات

تُعدّ مسألة SAT مهمة من الناحيتين النظرية والعملية. ففي نظرية التعقيد، كانت أول مسألة ثبت أنها من فئة NP-complete ، ويمكن أن تظهر في مجموعة واسعة من التطبيقات مثل التحقق من النماذج ، والتخطيط والجدولة الآليين ، والتشخيص في الذكاء الاصطناعي .

لذا، ظلّ تطوير برامج فعّالة لحلّ مسائل SAT موضوعًا بحثيًا لسنوات عديدة. وكان برنامج GRASP (1996-1999) من أوائل التطبيقات التي استخدمت تقنية DPLL. [ 1 ] وفي مسابقات SAT الدولية، حصدت تطبيقات تعتمد على DPLL، مثل zChaff [ 2 ] وMiniSat [ 3 ]، المراكز الأولى في مسابقات عامي 2004 و2005. [ 4 ]

ومن التطبيقات الأخرى التي غالباً ما تتضمن DPLL إثبات النظريات الآلي أو قابلية الإرضاء modulo النظريات (SMT)، وهي مشكلة SAT يتم فيها استبدال المتغيرات الافتراضية بصيغ نظرية رياضية أخرى .

الخوارزمية

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

تتفوق خوارزمية DPLL على خوارزمية التراجع من خلال الاستخدام الدقيق للقواعد التالية في كل خطوة:

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

يُكتشف عدم إمكانية تحقيق شرط جزئي معين إذا أصبح أحد بنوده فارغًا، أي إذا تم تعيين جميع متغيراته بطريقة تجعل القيم الحرفية المقابلة خاطئة. ويُكتشف إمكانية تحقيق الشرط إما عند تعيين جميع المتغيرات دون توليد البند الفارغ، أو، في التطبيقات الحديثة، عند تحقق جميع البنود. ولا يمكن اكتشاف عدم إمكانية تحقيق الشرط الكامل إلا بعد بحث شامل.

يمكن تلخيص خوارزمية DPLL في الشفرة الزائفة التالية، حيث Φ هي صيغة CNF :

خوارزمية DPLL المدخلات: مجموعة من البنود Φ. الناتج: قيمة منطقية تشير إلى ما إذا كانت Φ قابلة للتحقيق أم لا.
دالة DPLL (Φ) // انتشار الوحدة: بينما يوجد شرط وحدة { l } في Φ do Φ ← unit-propagate ( l , Φ); // الاستبعاد الحرفي البحت: بينما يوجد حرف l يحدث بشكل نقي في Φ do Φ ← pure-literal-assign ( l , Φ); // شروط التوقف: إذا كانت Φ فارغة، فأرجع القيمة true؛ وإذا كانت Φ تحتوي على عبارة فارغة، فأرجع القيمة false. // إجراء DPLL: ل ← اختيار الحرفي (Φ)؛ إرجاع DPLL (Φ ∧ {l}) أو DPLL (Φ ∧ {¬l});
  • يشير الرمز " ← " إلى عملية التخصيص . على سبيل المثال، " الأكبر ← عنصر " يعني أن قيمة الأكبر تتغير إلى قيمة العنصر .
  • " return " ينهي الخوارزمية ويخرج القيمة التالية.

في هذه الشفرة الزائفة، تُمثل الدالتان unit-propagate(l, Φ)و pure-literal-assign(l, Φ)دالتين تُعيدان نتيجة تطبيق قاعدة نشر الوحدة وقاعدة القيمة الحرفية البحتة، على التوالي، على القيمة الحرفية lوالصيغة Φ. بعبارة أخرى، تستبدلان كل ظهور لـ lبـ "صحيح" وكل ظهور لـ not lبـ "خطأ" في الصيغة Φ، مما يُبسط الصيغة الناتجة. orفي returnالعبارة هو عامل اختصار . يُشير إلى النتيجة المُبسطة لاستبدال بـ "صحيح" في .Φ ∧ {l}lΦ

ينتهي عمل الخوارزمية في إحدى حالتين: إما أن Φتكون صيغة CNF فارغة، أي لا تحتوي على أي شرط. في هذه الحالة، تُعتبر الصيغة مُحققة بأي عملية إسناد، لأن جميع شروطها صحيحة بشكل بديهي. أما إذا احتوت الصيغة على شرط فارغ، فإن هذا الشرط يكون خاطئًا بشكل بديهي، لأن الفصل يتطلب وجود عنصر واحد على الأقل صحيح لكي تكون المجموعة ككل صحيحة. في هذه الحالة، يعني وجود مثل هذا الشرط أن الصيغة (عند تقييمها كربط لجميع الشروط) لا يمكن أن تُقيّم إلى قيمة صحيحة، وبالتالي فهي غير قابلة للتحقيق.

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

تعتمد خوارزمية ديفيس-لوغمان-لوفلاند على اختيار متغير التفرع ، وهو المتغير الذي يُؤخذ في الاعتبار في خطوة التراجع. ونتيجةً لذلك، فهي ليست خوارزميةً بالمعنى الدقيق، بل هي مجموعة من الخوارزميات، واحدة لكل طريقة ممكنة لاختيار متغير التفرع. تتأثر الكفاءة بشدة باختيار متغير التفرع: فهناك حالات يكون فيها زمن التشغيل ثابتًا أو أُسّيًا اعتمادًا على اختيار متغيرات التفرع. تُسمى دوال الاختيار هذه أيضًا بالدوال الاستدلالية أو الاستدلالات التفرعية. [ 5 ]

الإضفاء الطابع الرسمي

يمكن استخدام الترميز المماثل لحساب المتتاليات لصياغة العديد من خوارزميات إعادة الكتابة، بما في ذلك DPLL. فيما يلي القواعد الخمس التي يمكن لمحلل DPLL تطبيقها إما لإيجاد أو عدم إيجاد تعيين مُرضٍ، أيأ=(ل1،¬ل2،ل3،...){\displaystyle A=(l_{1},\neg l_{2},l_{3},...)}[ 6 ] [ 7 ]​

إذا كان هناك بند في الصيغةΦ{\displaystyle \Phi }يحتوي على حرف واحد غير مُخصصل{\displaystyle l}فيأ{\displaystyle A}، مع ظهور جميع القيم الحرفية الأخرى في الجملة بشكل سلبي، قم بالتمديدأ{\displaystyle A}معل{\displaystyle l}تمثل هذه القاعدة فكرة أن العبارة الخاطئة حاليًا والتي تحتوي على متغير واحد غير مُحدد فقط تجبر على تعيين هذا المتغير بطريقة تجعل العبارة بأكملها صحيحة، وإلا فلن يتم استيفاء الصيغة .{ل1،...،لن،ل}∈Φ¬ل1،...،¬لن∈أل،¬ل∉أأ:=أل (نشر){\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n},l\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;l,\neg l\notin A\end{array}}{A:=A\;l}}{\text{ (Propagate)}}}إذا كان حرفيًال{\displaystyle l}يظهر في الصيغةΦ{\displaystyle \Phi }لكن نفيها¬ل{\displaystyle \neg l}لا يفعل، ول{\displaystyle l}و¬ل{\displaystyle \neg l}ليسوا فيأ{\displaystyle A}، يمتدأ{\displaystyle A}معل{\displaystyle l}تمثل هذه القاعدة فكرة أنه إذا ظهر متغير ما بشكل إيجابي بحت أو سلبي بحت في صيغة ما، فيمكن تعيين جميع الحالات إلى صحيح أو خطأ لجعل عباراتها المقابلة صحيحة.ل حرفيًا من Φ¬ل ليس حرفيًا من Φل،¬ل∉أأ:=أل (نقي){\displaystyle {\frac {\begin{array}{c}l{\text{ literal of }}\Phi \;\;\;\neg l{\text{ not literal of }}\Phi \;\;\;\;\;l,\neg l\notin A\end{array}}{A:=A\;l}}{\text{ (Pure)}}}إذا كان حرفيًال{\displaystyle l}هو ضمن مجموعة القيم الحرفية لـΦ{\displaystyle \Phi }ولال{\displaystyle l}ولا¬ل{\displaystyle \neg l}هو فيأ{\displaystyle A}ثم حدد قيمة الصواب لـل{\displaystyle l}وتوسيعأ{\displaystyle A}مع القرار الحرفي∙ل{\displaystyle \bullet l}تمثل هذه القاعدة فكرة أنه إذا لم تكن مجبرًا على القيام بمهمة ما، فيجب عليك اختيار متغير لتعيينه وتدوين المهمة التي تم اختيارها حتى تتمكن من الرجوع إذا لم يؤد الاختيار إلى مهمة مرضية .ل∈ليتس(Φ)ل،¬ل∉أأ:=أ∙ل (يقرر){\displaystyle {\frac {\begin{array}{c}l\in {\text{Lits}}(\Phi )\;\;\;l,\neg l\notin A\end{array}}{A:=A\;\bullet \;l}}{\text{ (Decide)}}}إذا كان هناك بند{ل1،...،لن}{\displaystyle \{l_{1},\dots ,l_{n}\}}هو فيΦ{\displaystyle \Phi }، ونفيها¬ل1،...،¬لن{\displaystyle \neg l_{1},\dots ,\neg l_{n}}فيأ{\displaystyle A}، وأ{\displaystyle A}يمكن تمثيلها على النحو التاليأ=أ′∙لشمال{\displaystyle A=A'\;\bullet \;l\;N}أين∙∉شمال{\displaystyle \bullet \notin N}ثم تراجع عن طريق التعيينأ{\displaystyle A}لأ′¬ل{\displaystyle A'\;\neg l}تمثل هذه القاعدة فكرة أنه إذا وصلت إلى تناقض في محاولة إيجاد مهمة صالحة، فأنت بحاجة إلى العودة إلى المكان الذي اتخذت فيه قرارًا سابقًا بين مهمتين واختيار المهمة الأخرى.{ل1،...،لن}∈Φ¬ل1،...،¬لن∈أأ=أ′∙لشمال∙∉شمالأ:=أ′¬ل (تراجع){\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n}\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;A=A'\;\bullet \;l\;N\;\;\;\;\;\bullet \notin N\end{array}}{A:=A'\;\neg l}}{\text{ (Backtrack)}}}إذا كان هناك بند{ل1،...،لن}{\displaystyle \{l_{1},\dots ,l_{n}\}}هو فيΦ{\displaystyle \Phi }، ونفيها¬ل1،...،¬لن{\displaystyle \neg l_{1},\dots ,\neg l_{n}}فيأ{\displaystyle A}ولا يوجد مؤشر للصراع∙{\displaystyle \bullet }فيأ{\displaystyle A}إذا لم يكن هناك أي شيء يمكن فعله بشكل مختلف في طريق الوصول إلى التناقض ، فإن خوارزمية DPLL تفشل. تمثل هذه القاعدة فكرة أنه إذا وصلت إلى تناقض ولكن لم يكن هناك أي شيء يمكنك فعله بشكل مختلف في طريقك إلى ذلك، فإن الصيغة غير قابلة للتحقيق.{ل1،...،لن}∈Φ¬ل1،...،¬لن∈أ∙∉أيفشل (يفشل){\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n}\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;\bullet \notin A\end{array}}{\text{Fail}}}{\text{ (Fail)}}}

التصور

قام ديفيس ولوغيمان ولوفلاند (1961) بتطوير هذه الخوارزمية. ومن خصائص هذه الخوارزمية الأصلية ما يلي:

  • يعتمد ذلك على البحث.
  • وهو الأساس لجميع برامج حل مسائل SAT الحديثة تقريبًا.
  • لا يستخدم التعلم أو التراجع غير الزمني (الذي تم تقديمه في عام 1996).

مثال مع تصور لخوارزمية DPLL التي تتضمن التراجع الزمني:

منذ عام 1986، تم استخدام مخططات القرار الثنائية (المرتبة المختزلة) أيضًا لحل SAT.

في عامي 1989-1990، تم تقديم طريقة ستالمارك للتحقق من الصيغ وحصلت على براءة اختراع. وقد وجدت بعض الاستخدامات في التطبيقات الصناعية. [ 8 ]

تم توسيع نطاق DPLL لإثبات النظريات الآلي لأجزاء من منطق الرتبة الأولى عن طريق خوارزمية DPLL(T) . [ 1 ]

خلال العقد الممتد من 2010 إلى 2019، أسفرت الجهود المبذولة لتحسين الخوارزمية عن إيجاد سياسات أفضل لاختيار المتغيرات المتفرعة وهياكل بيانات جديدة لتسريع الخوارزمية، لا سيما فيما يتعلق بنشر الوحدات . ومع ذلك، تمثل التحسين الرئيسي في خوارزمية أكثر قوة، وهي خوارزمية تعلم البنود المدفوعة بالتعارض (CDCL)، والتي تشبه خوارزمية DPLL، ولكنها بعد الوصول إلى تعارض، "تتعلم" الأسباب الجذرية (القيم المُسندة إلى المتغيرات) لهذا التعارض، وتستخدم هذه المعلومات لإجراء تراجع غير زمني (يُعرف أيضًا بالقفز العكسي ) لتجنب الوصول إلى نفس التعارض مرة أخرى. وتعتمد معظم برامج حل SAT الحديثة على إطار عمل CDCL اعتبارًا من عام 2019. [ 9 ]

العلاقة بالمفاهيم الأخرى

تتوافق عمليات تشغيل الخوارزميات القائمة على DPLL على الحالات غير القابلة للإرضاء مع براهين دحض حل الشجرة. [ 10 ]

انظر أيضاً

مراجع

عام

محدد

  1. 1 2 نيوفنهاوس، روبرت؛ أوليفرس، ألبرت؛ تينيلي، سيزار (2004)، "منطق DPLL المجرد ومنطق DPLL المجرد بنمط النظريات" (ملف PDF) ، وقائع المؤتمر الدولي حول المنطق للبرمجة والذكاء الاصطناعي والاستدلال ، LPAR 2004 ، الصفحات 36-50 
  2. ↑ موقع zChaff الإلكتروني
  3. ↑ "موقع مينيسات الإلكتروني" .
  4. ↑ صفحة الويب الخاصة بمسابقات SAT الدولية ، sat! live
  5. ^ ماركيز سيلفا، جواو ب. (1999). “تأثير الاستدلالات المتفرعة في خوارزميات الرضا المقترح”. في باراهونا، بيدرو؛ ألفيريس، خوسيه ج. (محرران). التقدم في الذكاء الاصطناعي: المؤتمر البرتغالي التاسع حول الذكاء الاصطناعي، EPIA '99 إيفورا، البرتغال، 21-24 سبتمبر، 1999 وقائع . LNCS . المجلد. 1695. ص 62 – 63. دوى : 10.1007 / 3-540-48159-1_5 . رقم ISBN   978-3-540-66548-9.
  6. ↑ نيوفنهاوس، روبرت؛ أوليفرس، ألبرت؛ تينيلي، سيزار (2006-11-01). "حل مسائل SAT وSAT Modulo Theories: من إجراء ديفيس-بوتنام-لوجمان-لوفلاند المجرد إلى DPLL(T)" . مجلة ACM . 53 (6): 937-977 . doi : 10.1145/1217856.1217859 . ISSN 0004-5411 . 
  7. ↑ كرستيتش، سافا؛ جويل، أميت (2007). كونيف، بوريس؛ وولتر، فرانك (محررون). "تصميم خوارزميات حل مسائل SAT Modulo Theories: Nelson-Oppen with DPLL" . آفاق أنظمة الدمج . برلين، هايدلبرغ: سبرينغر: 1-27 . doi : 10.1007/978-3-540-74621-8_1 . ISBN 978-3-540-74621-8.
  8. ↑ ستالمارك، ج.؛ سافلوند، م. (أكتوبر 1990). "نمذجة الأنظمة والبرمجيات والتحقق منها في منطق القضايا". مجلدات وقائع الاتحاد الدولي للتحكم الآلي . 23 (6): 31-36 . doi : 10.1016/S1474-6670(17)52173-4 .
  9. ↑ موهل، سيبيل؛ بير، أرمين (2019). "التراجع العكسي". نظرية وتطبيقات اختبار الإرضاء - SAT 2019 (ملف PDF) . سلسلة محاضرات في علوم الحاسوب. المجلد 11628. الصفحات 250-266 . doi : 10.1007/978-3-030-24258-9_18 . ISBN   978-3-030-24257-2. S2CID 195755607 . 
  10. ↑ فان بيك، بيتر (2006). "خوارزميات البحث بالتراجع" . في: روسي، فرانشيسكا؛ فان بيك، بيتر؛ والش، توبي (محررون). دليل برمجة القيود . إلسيفير. ص 122. ISBN  978-0-444-52726-4.

للمزيد من القراءة

  • مالاي غاني؛ آرتي غوبتا؛ د. آرتي غوبتا (2007). حلول التحقق الرسمي القابلة للتوسع القائمة على SAT . سبرينغر. ص 23-32 . ISBN  978-0-387-69166-4.
  • غوميز، كارلا ب.؛ كاوتز، هنري؛ سابهاروال، أشيش؛ سيلمان، بارت (2008). "حلول قابلية الإرضاء". في: فان هارميلين، فرانك؛ ليفشيتز، فلاديمير؛ بورتر، بروس (محررون). دليل تمثيل المعرفة . أسس الذكاء الاصطناعي. المجلد  3. إلسيفير. الصفحات 89-134 . doi : 10.1016/S1574-6526(07)03002-7 . ISBN  978-0-444-52211-5.