Solving Real-World Combinatorial Problems using High-Speed SAT-Algorithms

点击翻译按钮获取中文摘要

The purpose of this research is to develop general method for solving intractable real-world problems. Our strategy is not to solve each problem directly but to translate it into CNF Satis-fiability(SAT), solve SAT, and translate the solution of SAT back to the solution of the original problem. We can expect several advantages: (1) It is easy to translate combinatorial problems into SAT. (2) We can exploit existing fast SAT algorithms.In this research, we first formalized real-world problems and established translation method from real-world problems into SAT so that automatic translations are possible.Next, to examine the efficiency of our approach, we conducted experiments. We adopted the time-scheduling problem and the student assignment problem, which are popular problems in universities. Our experimental results show that for both problems our method performed better than existing direct algorithms.Finally, we attempted speedup of local search algorithms for SAT via parallelization. We used vector computer VPP 800and PVM for this purpose. The nature of local search algorithms fits for parallelization because we can run several search paths independently. Furthermore, we need little communication. By experiments, we showed that we can obtain ideal speedup as expected. We tried several benchmark instances and were able to solve some instances which had not been solved by any algorithms.