مسئله SAT
مسئله تصدقپذیری دودویی یا Boolean satisfiability problem که اصطلاحا به آن SATISFIABILITY یا مسئله SAT نیز گفته میشود. به این شکل هست که میپرسد آیا میتوان ارزش متغیر های یک گزاره (فرمول) دودویی را به گونه ای تعیین کرد که ارزش آن گزاره درست باشد؟ اگر بتوان چنین ارزش دهی ای را پیدا کنیم میگوییم آن گزاره صدق پذیر می باشد.
بعنوان مثال گزاره (A and ~B) یک گزاره صدق پذیر است زیرا اگر ارزش A را مساوی True و ارزش B را مساوی False در نظر بگیریم آنگاه گزاره فوق ارزش True را خواهد داشت. اما گزاره (A and ~A) یک گزاره تصدیق ناپذیر است .
مسئله SAT جزو اولین مسائلی بود که اثبات شد جزو مسائل Np-Complete می باشد. بنابراین یک الگوریتم کامل (الگوریتمی که رسیدن به پاسخ را تضمین کند) دارای زمان اجرایی است که در بدترین حالت بصورت نمایی با اندازه مسئله رشد میکند.
تعاریف :
یک گزاره منطقی از متغیرهای دودویی و3 عملگر And و Or و Not و همچنین پرانتز تشکیل شده است.
clause (عبارت) : یک clause عبارتی است شامل عملگر OR و NOT یعنی در آن متغیر های یا نقیض متغیرها با یکدیگر OR میشوند.
مانند عبارت : , x1 ∨ ¬x2 به بیان دیگر یک Clause یک فصل منطقی از متغیرها می باشد.
CNF : یک عبارت به صورت CNF یا conjunctive normal form می باشد اگر تعدادی clause را با هم AND کرده باشد.
بعنوان مثال :
(x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1
جهت انجام پروژه در خصوص مسئله SAT با انواع الگوریتم های هوشمند و تکاملی با ما تماس بگیرید:
شماره تماس: 09120563264 (تلگرام و واتس اپ)
ایمیل : matlab24ir@gmail.com و یا info@matlab24.ir
حل مسئله 3-SAT با الگوریتم GSAT .
حل مسئله 3-SAT با الگوریتم WalkSAT .
حل مسئله 3-SAT با الگوریتم ژنتیک .
حل مسئله 3-SAT با الگوریتم PSO .
حل مسئله 3-SAT با الگوریتم ABC .
حل مسئله 3-SAT با الگوریتم DE .
