سیدمحسن موسوی - بروجرد، دانشگاه آزاد اسلامی دانشکده تحصیلات تکمیلی، گروه مهندسی کامپیوتر
سیدرسول موسوی - تهران، دانشگاه صنعتی امیرکبیر، گروه مهندسی کامپیوتر

هدف در مسائل بهینه سازی، بیشینه (و یاکمینه) کردن مقدار یک تابع بر حسب یک متغیر، است. یکی از روش هایکارآمد جهت حل این مسائل، مدل کردن مسئله به مسئله مشهور ارضاپذیری بیشینه بولی یا به اختصار SAT-Maxمی باشد. لذا مسائل متعددی از دنیای علوم و صنایع برای حل، ابتدا به این مسئله مدل شده و سپس با الگوریتم های حلاین مسئله، حل می شوند. ورودی این مسئله یک عبارت منطقی است که معمولا در فرم نرمال عطفی 2 است و در آن،تعداد n متغیر به صورت لیترال مثب یا منفی، در تعداد m جمله ظاهر شده اند. در مسئله Max-SAT هدف آنست کهمتغیرها را طوری مقداردهی کنیم که ارزش بیشترین تعداد ممکن از جمله های عبارت ورودی، برابر با 'True' شود. باتوجه به NP-Hard بودن این مسئله از یک سو و کاربردی بودن آن از سوی دیگر، الگوریت های بسیاری جهت حلMax-SAT ارائه شده است . به نسخه پیاده سازی شده ا گوریتم های حل مسئله، سالور می گویند. در این مقاله یکالگوریتم ابداعی برای حل این مسئله، ارائه شده است . در این الگوریتم از جستجوی محلی تکرار شونده یا به اختصارILS به عنوان چارچوب کار برای گونه ای جستجوی تپه نوردی ( VHC) استفاده شده است. مقداردهی اولیه متغیرها،به صورت تصادمی صورت نگرفته و مکانیزمی جهت تقویت مقوله تنوع در برابر مقو له تشدید، در این الگوریتم تعبیهشده است. ایده ما در سالوری ابداعی به نام MILS پیاده سازی شده است. در فاز ارزیابی data set، برخی مسائل مدلشده از مبحث بیوانفورماتیک است. MILS در برابر سالور مشهور IRoTS ارزیابی شده و خوشبختانه تجربیات عملی،موید برتری MILS است.

ارضاپذیری بیشینه بولی، جستجوی محلی، هیوریستیک، بیوانفورماتیک