![cover image](https://wikiwandv2-19431.kxcdn.com/_next/image?url=https://upload.wikimedia.org/wikipedia/commons/thumb/d/dc/Dpll11.png/640px-Dpll11.png&w=640&q=50)
الگوریتم DPLL
From Wikipedia, the free encyclopedia
الگوریتم DPLL (کوتهنوشت Davis–Putnam–Logemann–Loveland) در منطق و علوم رایانه، یک الگوریتم جستجوی کامل و مبتنی بر پسگرد برای تصمیمگیری درمورد صدقپذیری برای فرمولهای منطق گزارهای در حالت نرمال عطفی است، به عبارت دیگر الگوریتم DPLL دارد مسئله CNF-SAT را حل میکند.
![]() در یک فرمول CNF-SAT این مراحل را انجام دهید:
۱-یک لیترال را انتخاب کنید، ۲- یک مقدار درستی به آن منتسب کنید، ۳-فرمول را ساده کنید، ۴-صدقپذیری را بررسی کنید، ۵-اگر صادق نیست، پسگرد انجام دهید. | |
رده | مسئله صدقپذیری دودویی |
---|---|
ساختمان داده | درخت دودویی |
کارایی بدترین حالت | |
کارایی بهترین حالت | |
پیچیدگی فضایی |
این الگوریتم در سال ۱۹۶۱ توسط مارتین دیویس، جرج لاگِمن، و دونالد لاولند معرفی گردید، که یک روش اصلاحی برای الگوریتم پیشین دیویس-پاتنام بود. بخصوص در نشریات قدیمی، به الگوریتم دیویس-پاتانم-لاولند، «روش دیویس-پاتنام» یا «الگوریتم DP» گفته میشد. نامهای معمولتر دیگری که این تفاوت را حفظ نمودهاند، DLL و DPLL میباشند.
بعد از حدود ۵۰ سال، هنوز هم فرایند DPLL مبنایی برای موثرترین حلکنندههای کامل SAT میباشد. این الگوریتم، امروزه، این الگوریتم، در زمینه اثبات قضیه خودکار برای قطعههایی از منطق مرتبه اول، به روش الگوریتم DPLL(T) گسترش داده شدهاست.[1]