advertise laitec sharif univercity تبلیغات در سایت سورس کد تبلیغات در سایت سورس کد
پروژه کامل مدیریت شرکت نرم افزاری با سی شارپ و SQL

پروژه کامل مدیریت شرکت نرم افزاری با سی شارپ و SQL

15000 تومان
دانلود پروژه فروشنده دوره گرد با الگوریتم گرانشی در #C

دانلود پروژه فروشنده دوره گرد با الگوریتم گرانشی در #C

4800 تومان
دانلود سورس پروژه TSP با الگوریتم مورچگان Ants

دانلود سورس پروژه TSP با الگوریتم مورچگان Ants

4800 تومان
دانلود سورس n وزیر با جست وجوی ممنوع در سی شارپ #C

دانلود سورس n وزیر با جست وجوی ممنوع در سی شارپ #C

3000 تومان
دانلود آپلود سنتر پیشرفته با PHP و Ajax

دانلود آپلود سنتر پیشرفته با PHP و Ajax

3000 تومان

الگوریتم دیویس پوتنام 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