Skip to main content
SUPERVISOR
Keyarash Bazargan,Seyed Rasul Moosavi
کیارش بازرگان (استاد راهنما) سید رسول موسوی (استاد راهنما)
 
STUDENT
Abdorrahim Bahrami
عبدالرحیم بهرامی

FACULTY - DEPARTMENT

دانشکده مهندسی برق و کامپیوتر
DEGREE
Master of Science (MSc)
YEAR
1385

TITLE

Implementation and Modification to Algorithms for Satisfiability Problem and some of its variants
In the theory of computation, decision problems are divided into two different groups of decidable and undecidable problems. A decidable problem is one which is solvable; that is, an algorithm can be devised to solve it. It is undecidable otherwise. Decidable problems are further divided into several groups based on the complexity of their solutions. There are problems for which PTIME algorithms exist. Such problems belong to the complexity dir=ltr There exist, however, problems neither proved nor disproved to be in P. All NP-complete problems, and some other NP-hard ones, are among such problems. The Boolean Satisfiability (SAT) problem was the first problem shown to be NP-complete. It is to decide, given a Boolean formula, whether there exists a variable assignment which 'satisfies' the formula, i.e. make is true. All NP-complete problems are efficiently reducible to each other. Therefore, if one of them can be solved in polynomial order of the problem size, all of them can be solved with this order. The NP-hard dir=ltr The goal of this project is to investigate and improve some of the SAT and Max-SAT algorithms. Firstly, the SAT problem and some of its algorithms are studied. Then, the reduction of SAT to other NP-complete problems with relatively quick algorithms is investigated. Although such a reduction is performed in PTIME, the size of the problem instance increases significantly by each reduction. Another method, called interval method, was then proposed and implemented. In the interval method, each variable assignment is represented as a binary number, each bit representing the value of a variable. A special search algorithm is then used to find a satisfying assignment, if any, in the state space of different values for the binary number. Special pruning techniques are used to reduce the size of the state space. A hardware circuit was also designed and tested for some small instances. However, none of these methods was successful in achieving a fast reliable solution to the problem. However, a successful method proposed in this thesis is to preprocess the given SAT instance using a simplification algorithm. The algorithm operates on the input instance and given, as its output, a simplified, yet equivalent, instance. Experiments, based on some standard SAT solvers, shows that the proposed algorithm can remarkably reduce the amount of time required to solve the problem. In particular, the algorithms reduced by about 25% the run time of two popular sat solvers, namely Rsat and Minisat, over several standard benchmarks. In this thesis, in addition to the SAT decision problem, the MAX-SAT optimization problem was investigated. Initially, a new heuristic algorithm called K-Half-SAT was propose... Key Words Satisfiability Problem, Backtracking, Branch and Bound, Simplification Algorithm, Local Search, Hill Climbing
در تئوری محاسبات مسائل تصمیم گیری به دو دسته تصمیم پذیر و تصمیم ناپذیر تقسیم می شوند. یک مسئله تصمیم پذیر مسئله ای است که قابل حل باشد به این معنی که بتوان یک الگوریتم برای آن طراحی کرد، در غیر این صورت مسئله مورد نظر تصمیم ناپذیر خواهد بود. مسائل تصمیم پذیر به نوبه خود و با توجه به مرتبه زمانی حل خود به دسته های متفاوتی تقسیم می شوند. دسته ای از آنها مسائلی هستند که برای آنها الگوریتمی با مرتبه زمانی چند جمله ای موجود می باشد. این مسائل به کلاس مرتبه زمانی P تعلق دارند. از طرف دیگر مسائلی وجود دارند که اثبات شده است الگوریتمی با مرتبه زمانی چند جمله ای برای آنها وجود ندارد. همچنین مسائلی وجود دارند که تعلق یا عدم تعلق آنها به کلاس P اثبات نشده است. تمام مسائل NP-Complete و برخی از مسائل NP-Hard از این دسته مسائل می باشند. مسئله ارضاءپذیری (SAT) اولین مسئله ای بود که NP-Complete بودن آن اثبات شد. هدف این مسئله تشخیص وجود یا عدم وجود یک مقداردهی برای متغیرها به نحوی که یک عبارت منطقی داده شده مقدار true بگیرد، می باشد. تمام مسائل NP-Complete به طور مؤثری قابل کاهش به یکدیگر می باشند. بنابراین اگر یکی از آنها با یک مرتبه زمانی چند جمله ای بر حسب اندازه مسئله حل شود، تمامی آنها با این مرتبه زمانی قابل حل خواهند بود. کلاس NP-Hard شامل بسیاری از مسائل بهینه سازی از جمله مسئله Max-SAT می باشد، که این مسئله گونه بهینه سازی مسئله ارضاءپذیری می باشد. هدف این پروژه بررسی و بهبود برخی از الگوریتم های مسائل SAT و Max-SAT می باشد. در ابتدا مسئله SAT و برخی از الگوریتم های آن مورد بررسی قرار گرفتند. سپس کاهش مسئله SAT به دیگر مسائل NP-Complete با الگوریتم های نسبتاً سریع مورد بررسی قرار گرفت. اگر چه کاهش پذیری با الگوریتمی با مرتبه زمانی چند جمله ای صورت می گرفت، اما اندازه نمونه مسئله با هر کاهش به طور مؤثری افزایش می یافت. سپس روش دیگری که روش بازه ای نامیده شد، پیشنهاد و مورد بررسی قرار گرفت. در روش بازه ای هر مقداردهی به متغیرها به صورت یک عدد در مبنای دو نمایش داده شد، هر بیت نشان دهنده مقدار یک متغیر بود. سپس یک جستجوی ویژه برای پیدا کردن یک مقداردهی درست در صورت وجود بر روی فضای حالت مقادیر مختلف عدد دودویی مربوطه انجام گرفت. روش های هرس کردن متفاوت و ویژه ای برای کاهش اندازه فضای حالت مورد استفاده قرار گرفت. همچنین یک مدار سخت افزاری طراحی شد و بر روی چند نمونه مورد آزمایش قرار گرفت. به هر حال هیچ یک از این روش ها در به دست آوردن یک راه حل سریع قابل اعتماد برای این مسئله موفق نبودند. به هر حال یک روش موفق در این پروژه پیشنهاد شد که در آن یک نمونه مسئله SAT با استفاده از یک الگوریتم ساده سازی مورد پیش پردازش قرار می گرفت. الگوریتم مورد نظر بر روی نمونه ورودی عمل کرده و یک نمونه ساده تر و در عین حال معادل را به ......... واژه های کلیدی مسئله ارضاءپذیری، بازگشت به عقب، شاخه و حد، الگوریتم ساده سازی، جستجوی محلی، تپه نوردی

ارتقاء امنیت وب با وف بومی