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

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

بيانات عامّة

الصنف	خوارزمية بحث
تاريخ الاكتشاف	1962
نسبة التسمية	مارتن ديفيس

خوارزمية ديفيس–بوتنام–لوغيمان–لوفلاند (بالإنجليزية: Davis–Putnam–Logemann–Loveland) هي خوارزمية بحث كاملة تعتمد على الاسترجاع الخلفي، وتُستخدم في مجالَي المنطق وعلوم الحاسوب لحل مسألة الاستيفاء المنطقي لحساب القضايا المكتوبة على الصيغة العادية التوافقية.

طُورت الخوارزمية في عام 1961 على يد مارتن ديفيس، وجورج لوغيمان، ودونالد لوفلاند، بوصفها تطويرًا لخوارزمية سابقة تُعرف بـ خوارزمية ديفيس–بوتنام، التي أُقترحت عام 1960 من قِبل ديفيس وهيلاري بوتنام، وكانت تعتمد على أسلوب الاستنتاج بالتوسيط.

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

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

ونظرًا لأهميتها، شكّل تطوير محلّلات فعالة لهذه المسألة موضوعًا بحثيًا لسنوات عديدة. يُعد نظام البحث الشامل عبر الفضاء الاحتمالي الذي طُوّر ما بين عامي 1996 و1999 من أوائل التنفيذات التي استخدمت خوارزمية ديفيس–بوتنام–لوغيمان–لوفلاند.^[1]

في المسابقات الدولية لمشكلات الاستيفاء المنطقي، تصدرت البرامج المعتمدة على هذه الخوارزمية، مثل تشاف زد،^[2] وميني سات،^[3] المراتب الأولى في نسختي عامي 2004 و2005. كما تُستخدم الخوارزمية على نطاق واسع في تطبيقات أخرى، منها الإثبات الآلي للنظريات، ومسائل الإرضاء وفق نظريات رياضية مختلفة، حيث تُستبدل المتغيرات الافتراضية بصيغ تنتمي إلى نظريات مثل الحساب الخطي أو نظرية الأعداد.