advertise laitec sharif univercity تبلیغات در سایت سورس کد تبلیغات در سایت سورس کد
سورس پروژه دفترچه تلفن ساده در سی شارپ #c و بانک Access

سورس پروژه دفترچه تلفن ساده در سی شارپ #c و بانک Access

3000 تومان
پروژه پایانی PHP وب سایت فروشگاه کامپیوتری

پروژه پایانی PHP وب سایت فروشگاه کامپیوتری

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

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

3000 تومان
دانلود پروژه پایانی طراحی وب سایت مخابرات با Asp.net

دانلود پروژه پایانی طراحی وب سایت مخابرات با Asp.net

14000 تومان
دانلود پروژه مهندسی نرم افزار ، نمایندگی ایران خودرو

دانلود پروژه مهندسی نرم افزار ، نمایندگی ایران خودرو

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

سفارش پروژه در سورس کد

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

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