خوارزمية ديفيس-بوتنام

الموسوعة الحرة

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

ملخص

جولتان من إجراء ديفيس-بوتنام على أمثلة لحالات أرضية افتراضية. من الأعلى إلى الأسفل، من اليسار: بدءًا من الصيغة(أ∨ب∨ج)∧(ب∨¬ج∨¬و)∧(¬ب∨هـ){\displaystyle (a\lor b\lor c)\land (b\lor \lnot c\lor \lnot f)\land (\lnot b\lor e)}، تقوم الخوارزمية بالحل علىب{\displaystyle b}ثم علىج{\displaystyle c}بما أنه لا يمكن التوصل إلى حل إضافي، تتوقف الخوارزمية؛ ولأن الشرط الفارغ لم يُستنتج، فإن النتيجة " قابلة للإرضاء ". على اليمين: حل الصيغة المعطاة علىب{\displaystyle b}ثم علىأ{\displaystyle a}ثم علىج{\displaystyle c}ينتج عنه عبارة فارغة؛ وبالتالي فإن الخوارزمية تُرجع " غير قابل للتنفيذ ".

تعتمد هذه الطريقة على نظرية هيربراند ، التي تنص على أن الصيغة غير القابلة للإرضاء لها حالة أساسية غير قابلة للإرضاء ، وعلى حقيقة أن الصيغة تكون صحيحة إذا وفقط إذا كان نفيها غير قابل للإرضاء. وبناءً على ذلك، فإن إثبات صحة الصيغة φ يتطلب إثبات أن الحالة الأساسية للصيغة ¬φ غير قابلة للإرضاء. إذا كانت الصيغة φ غير صحيحة، فلن ينتهي البحث عن حالة أساسية غير قابلة للإرضاء.

تتكون إجراءات التحقق من صحة الصيغة φ تقريبًا من هذه الأجزاء الثلاثة:

  • ضع الصيغة ¬φ في شكل prenex واحذف المحددات الكمية
  • قم بإنشاء جميع حالات الأساس الافتراضي، واحدة تلو الأخرى
  • تحقق مما إذا كانت كل حالة قابلة للتنفيذ.
    • إذا كانت إحدى الحالات غير قابلة للتحقيق، فأرجع أن φ صالحة. وإلا فتابع التحقق.

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

خوارزمية حل مشكلة الرضا الديناميكي (DP SAT) المدخلات: مجموعة من البنود Φ. الناتج: قيمة الصواب: صحيح إذا كان من الممكن تحقيق Φ، خطأ خلاف ذلك.
دالة DP-SAT(Φ) تكرار // نشر الوحدة: طالما أن Φ تحتوي على عبارة وحدة { l } do لكل عبارة c في Φ تحتوي على l do Φ ← remove-from-formula ( c , Φ); لكل عبارة c في Φ تحتوي على ¬ l do Φ ← remove-from-formula ( c , Φ); Φ ← إضافة إلى الصيغة ( c \ {¬ l }, Φ)؛ // حذف العبارات غير الموجودة في الشكل الطبيعي: لكل عبارة c في Φ تحتوي على كل من l الحرفي ونفيه ¬ l do Φ ← remove-from-formula ( c , Φ ); // الحذف الحرفي البحت: طالما أن هناك حرف l، فإن جميع حالاته في Φ لها نفس القطبية، قم بما يلي لكل جملة c في Φ تحتوي على l: Φ ← remove-from-formula ( c , Φ)؛ // شروط التوقف: إذا كانت Φ فارغة، فأرجع القيمة true؛ إذا كانت Φ تحتوي على عبارة فارغة، فأرجع القيمة false؛ // إجراء ديفيس-بوتنام: اختر حرفًا l يظهر مع كلا القطبين في Φ لكل جملة c في Φ تحتوي على l وكل جملة n في Φ تحتوي على نفيها ¬ l do // حل c مع n: r ← ( c \ { l }) ∪ ( n \ {¬ l }); Φ ← إضافة إلى الصيغة ( r , Φ)؛ لكل جملة c تحتوي على l أو ¬ l قم بما يلي: Φ ← إزالة من الصيغة ( c , Φ)؛
  • يشير الرمز " ← " إلى عملية التخصيص . على سبيل المثال، " الأكبر ← عنصر " يعني أن قيمة الأكبر تتغير إلى قيمة العنصر .
  • " return " ينهي الخوارزمية ويخرج القيمة التالية.

في كل خطوة من خطوات حل مشكلة SAT، تكون الصيغة الوسيطة الناتجة قابلة للإرضاء بنفس القدر ، ولكنها قد لا تكون مكافئة للصيغة الأصلية. وتؤدي خطوة الحل إلى تضخم أُسّي في أسوأ الحالات في حجم الصيغة.

خوارزمية ديفيس -بوتنام-لوغمان-لوفلاند هي تحسينٌ أُدخل عام ١٩٦٢ على خطوة إرضاء القضايا في إجراء ديفيس-بوتنام، وهي لا تتطلب سوى مقدار خطي من الذاكرة في أسوأ الحالات. تتجنب هذه الخوارزمية قاعدة التقسيم ، إذ تعتمد على خوارزمية تراجع تختار قيمة حرفية l ، ثم تتحقق بشكل متكرر مما إذا كانت الصيغة المبسطة التي تُسند فيها قيمة صحيحة لـ l قابلة للإرضاء، أو ما إذا كانت الصيغة المبسطة التي تُسند فيها قيمة خاطئة لـ l قابلة للإرضاء. ولا تزال هذه الخوارزمية تُشكل أساسًا لأكثر خوارزميات حل مسائل الإرضاء الكاملة كفاءةً حتى اليوم (حتى عام ٢٠١٥) .

انظر أيضاً

مراجع