الگوریتم دیویس پوتنام DPLL
الگوریتم دیویس پوتنام DPLL
الگوریتم (DPLL (Davis-Putnam algorithm متکی به الگوریتم جست وجوی عقبگرد است که از الگوریتم های کارآمد در استنتاج گزاره ای مبتنی بر بازرسی مدل میباشد. این الگوریتم به بررسی قابلیت ارضا شدن، یعنی مساله SAT مربوط میشود.
الگوریتم DPLL) DPLL حروف اول نام افرادی است که آن را طراحی کرده اند )، جمله ای را به شکل نرمال عطفی، (مجموعه ای از کلازها) دریافت میکند. همانند BACKTRACKING-SEARCH و TT-ENTAILS?، این الگوریتم نیز به طور بازگشتی مدل های ممکن را به صورت عمقی شمارش میکند. نسبت به TT-ENTAILS? سه تغییر دارد:
♦ خاتمه زودهنگام :
الگوریتم، حتی در یک مدل نیمه کامل، مشخص میکند آیا جمله باید درست باشد یا نادرست. کلاز وقتی درست است که تمام لیترال های آن درست باشد، حتی اگر لیترال های دیگر هنوز فاقد "مقادیر درستی" باشند. لذا قبل از کامل شدن مدل، میتوان نتیجه گرفت کل جمله درست است. بطور مشابه جمله وقتی نادرست است که تمام کلازهای آن نادرست باشد و کلاز وقتی نادرست است که هر یک از لیترال های ان نادرست باشند. قبل از کامل شدن مدل میتوان به این نتیجه رسید. خاتمه زودهنگام، تمام زیردخت های فضای جست وجو را بررسی نمیکند.
♦ ابتکار نماد محض :
نماد محض، نمادی است که در تمام کلازها با علامت یکسانی ظاهر میشود (مثبت یا منفی). اگر جمله ای دارای مدل باشد، در آن مدل نمادهای محض طوری انتساب داده شده اند که لیترال های آن را "درست" میکند. زیرا به این ترتیب، یک کلاز هرگز نادرست نخواهد بود. در تعیین محض بودن یک نماد، الگوریتم میتواند در مدلی که تاکنون ساخته شده است، از کلازهایی که قبلا بعنوان کلازهای درست شناخته شده اند، صرفنظر کند.
♦ ابتکار کلاز واحد :
کلاز واحد بعنوان کلازی تعریف شده است که فقط یک لیترال دارد. این ها در DPLL کلازهایی هستند که تمام لیترال های آن، به جز یک لیترال توسط مدل ارزش نادرستی پیدا کرده اند.
شبه کد الگوریتم DPLL را در ادامه خواهید دید. ساختار اصلی الگوریتم نشان داده شده که فرآیند جست وجو را توصیف میکند.
آنچه که این الگوریتم انجام میدهد، تکنیک هایی که حل کننده های SAT را قادر میسازد تا مسئله های بزرگتر را حل کنند، ارائه نمیکند. بسیاری از این تکنیک ها کلی هستند و قبلا آنها را در قالب های دیگری بیان کرده ایم:
► تجزیه و تحلیل مولفه : وقتی DPLL مقادیر درستی را به متغیرها نسبت میدهد، ممکن است مجموعه ای از عبارات، به زیر مجموعه های جدا از هم، به نام مولفه تبدیل شوند، که هیچ متغیر بدون انتسابی بین انها مشترک نیت. با توجه به یک روش کارآمد برای تشخیص وضوح این وضعیت، حل کننده میتواند با کار کردن جداگانه بر روی هر مولفه با سرعت زیادی عمل کند.
► تعیین ترتیب متغیرها و مقادیر : پیاده سازی ساده DPLL از ترتیب دلخواهی برای متغیرها استفاده میکند و همیشه مقدار true را قبل از false تست میکند.
► عقبگرد هوشمند : بسیاری از مسئله ها که نمیتوانند با عقبگرد زمانی در چندین ساعت حل شوند، با عقبگرد هوشمند میتوانند در چند ثانیه حل شوند. این روش مسیر را تا نقطه تناقض مرتبط به عقب برمیگرداند. تمام حل کننده های SAT که عقبگرد هوشمند را انجام میدهند برای ثبت برخوردها از یادگیری کلاز تناقض استفاده میکنند، تا بعدا در عمل جست وجو، آن را تکرار نکنند.
► شروع مجدد تصادفی : گاهی اجرای الگوریتم متوقف میشود و ادامه پیدا نمیکند. در این صورت به جای تلاش برای ادامه کار پس از شروع مجدد انتخاب های تصادفی مختلفی انجام میشود. کلازهایی که در اجرای اول یادگرفته میشوند، پس از شروع مجدد نگهداری میشوند و این کار میتواند به هرس فضای جست وجو کمک کند.
► شاخص گذاری هوشمند : روش های سریعی که در خود DPLL استفاده شدند، به شاخص گذاری چیزهایی مثل مجموعه ای از کلاز ها که در آنها متغیرهای Xi بصورت لیترال مثبت ظاهر میشود نیاز دارند. ساختارهای شاخص گذاری باید در حین انجام محاسبات به هنگام شوند.
با این بهبودهایی که حاصل شد، حل کننده های مدرن میتوانند مسئله هایی با ده ها میلیون متغیر را حل کنند. آنها میتوانند سخت افزار و پروتکل های امنیتی را بررسی و بازبینی کنند.
شبه کد الگوریتم DPLL
function DPLL-SATISFIABLS?(s) returns true or false
inputs : s, a sentence in propositional logic
clauses <-- the set of clauses in the CNF representation of s
symbols <-- a list of the proposition symbols in s
return DPLL(clauses, symbols, {} )
function DPLL(clauses, symbols, model) returns true or false
if every clause in clauses is true in model then return true
if some clause in clauses is true in model then return false
P,value <-- FIND-PURE-SYMBOL (clauses, symbols, model
if P is non-null then return DPLL(clauses, symbols - P, model U {P = value} )
P,value <-- FIND-UNIT-CLAUSE (clauses, model)
if P is non-null then return DPLL(clauses, symbols - P, model U {P = value} )
P <-- FIRST (symbols) ; rest <-- REST(symbols)
return DPLL(clauses, rest, model U {P = true} ) or DPLL(clauses, rest, model U {P = false} )
