پياده سازي و بهبود الگوريتم هايي براي مسئله ارضا پذيري و گونه هايي از آن

چكيده انگليسي :

Implementation and Modification to Algorithms for Satisfiability Problem and some of its variants Abdorrahim Bahrami abdorrahim@ec iut ac ir February 15 2007 Department of Electrical and Computer Engineering Isfahan University of Technology Isfahan 84156 83111 Iran Degree M Sc Language Persian Seyed Rasoul Mousavi srm@cc iut ac ir Kiarash Bazargan kiarash@cc iut ac irAbstractIn the theory of computation decision problems are divided into two different groups of decidable andundecidable problems A decidable problem is one which is solvable that is an algorithm can be devised tosolve it It is undecidable otherwise Decidable problems are further divided into several groups based on thecomplexity of their solutions There are problems for which PTIME algorithms exist Such problems belongto the complexity class P On the other hand there exist problem proved not to have any PTIME algorithms There exist however problems neither proved nor disproved to be in P All NP complete problems andsome other NP hard ones are among such problems The Boolean Satisfiability SAT problem was the firstproblem shown to be NP complete It is to decide given a Boolean formula whether there exists a variableassignment which satisfies the formula i e make is true All NP complete problems are efficiently reducibleto each other Therefore if one of them can be solved in polynomial order of the problem size all of themcan be solved with this order The NP hard class includes many optimization problems including Max SAT which is an optimization variant of the SAT problem The goal of this project is to investigate and improve some of the SAT and Max SAT algorithms Firstly theSAT problem and some of its algorithms are studied Then the reduction of SAT to other NP completeproblems 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 intervalmethod was then proposed and implemented In the interval method each variable assignment is representedas a binary number each bit representing the value of a variable A special search algorithm is then used tofind a satisfying assignment if any in the state space of different values for the binary number Specialpruning techniques are used to reduce the size of the state space A hardware circuit was also designed andtested for some small instances However none of these methods was successful in achieving a fast reliablesolution to the problem However a successful method proposed in this thesis is to preprocess the given SAT instance using asimplification 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 proposedalgorithm can remarkably reduce the amount of time required to solve the problem In particular thealgorithms reduced by about 25 the run time of two popular sat solvers namely Rsat and Minisat overseveral standard benchmarks In this thesis in addition to the SAT decision problem the MAX SAT optimization problem wasinvestigated Initially a new heuristic algorithm called K Half SAT was proposed and compared with analgorithm based on the Ant Colony Optimization Then a recent competent solver called Maxsatz wasinvestigated implemented and improved by incorporating a local search algorithm The resulting algorithmwhich is a hybrid of Branch and Bound and Hill Climbing was expected to pride a better pruning of thesearch tree It was compared with the original algorithm with positive results over a number of standardbenchmarks Key WordsSatisfiability Problem Backtracking Branch and Bound Simplification Algorithm LocalSearch Hill Climbing

بهرامي، عبدالرحيم

پياده سازي و بهبود الگوريتم هايي براي مسئله ارضا پذيري و گونه هايي از آن

بازگشت به عقب , شاخه و حد , الگوريتم ساده سازي , جستجوي محلي , تپه نوردي