advertise laitec sharif univercity استخراج بیت کوین با کامپیوتر استخراج بیت کوین با کامپیوتر
سیستم اتوماسیون دهیاری ، پروژه مهندسی نرم افزار

سیستم اتوماسیون دهیاری ، پروژه مهندسی نرم افزار

3000 تومان
دانلود سورس پروژه فروشگاه کیف با asp.net و sql express

دانلود سورس پروژه فروشگاه کیف با asp.net و sql express

3000 تومان
دانلود مقاله ای در مورد الگوریتم  کرم شب تاب FireFly در هوش مصنوعی

دانلود مقاله ای در مورد الگوریتم کرم شب تاب FireFly در هوش مصنوعی

3000 تومان
دانلود سورس پروژه پایانی وب سایت بنگاه املاک با php

دانلود سورس پروژه پایانی وب سایت بنگاه املاک با php

18000 تومان
سورس پروژه پایانی آزمون گیری با زبان سی شارپ و SQL

سورس پروژه پایانی آزمون گیری با زبان سی شارپ و SQL

7000 تومان

الگوریتم دیویس پوتنام DPLL

الگوریتم (DPLL (Davis-Putnam algorithm متکی به الگوریتم جست وجوی عقبگرد است که از الگوریتم های کارآمد در استنتاج گزاره ای مبتنی بر بازرسی مدل میباشد. این الگوریتم به بررسی قابلیت ارضا شدن، یعنی مساله SAT مربوط میشود.
الگوریتم دیویس پوتنام DPLL

الگوریتم دیویس پوتنام DPLL

الگوریتم (DPLL (Davis-Putnam algorithm متکی به الگوریتم جست وجوی عقبگرد است که از الگوریتم های کارآمد در استنتاج گزاره ای مبتنی بر بازرسی مدل میباشد. این الگوریتم به بررسی قابلیت ارضا شدن، یعنی مساله SAT مربوط میشود.

الگوریتم DPLLDPLL حروف اول نام افرادی است که آن را طراحی کرده اند )، جمله ای را به شکل نرمال عطفی، (مجموعه ای از کلازها) دریافت میکند. همانند 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} )  

 

 



0
نظرات

نظر خود را ارسال کنید



نام:
ایمیل:
دیدگاه:
captcha
کد امنیتی :


advertise
آموزش الگوریتم دیویس پوتنامالگوریتم DPLL چگونه عمل میکند؟روش کار الگوریتم دیویس پوتنام چگونه است؟DPLL Davis-Putnam algorithmشبه کد الگوریتم DPLLآشنایی با الگوریتم عقبگرد دیویس پوتنامتبلیغات ارزان سایت آموزش برنامه نویسیتبلیغات مخصوص طراحان وب سایتتبلیغات در سایت برنامه نویسیتبلیغات اینترنتی برای برنامه نویساندر آغوش مینیمالیسممنوی همبرگر با سه خط افقی که روی یکدیگر قرار گرفته اند نشانه چیست؟ سوئیچ به یک ستون واحدتبدیل متن ساده به وبلاگ و سایت های پویا با React.jsکتابخانه sass برای استفاده آسان تر از آنکتابخانه سطح بالا برای اتوماتیک سازی اعمال مرورگر لیست برچسب ها
تمامی حقوق این سایت اعم از محتوی ، تصاویر ، قالب و ... متعلق به گروه مهندسی وب سایت سورس کد می باشد.
SourceCodes.ir ، افقی روشن برای برنامه نویسان ، از مبتدی تا حرفه ای

کسب درآمد با کامپیوتر
تولید بیت کوین با کامپیوتر

پیشنهادات ویژه سورس کد

پکیج ویژه پروژه پایانی رشته کامپیوتر دانلود مجموعه 70 پروژه کاربردی سی شارپ وب سایت فروشگاه با php