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

本研究的目的是开发解决现实世界中棘手问题的通用方法。我们的策略不是直接求解每个问题，而是将其转化为CNF可满足性（SAT），求解SAT，并将SAT的解转化为原问题的解。我们可以预期几个优点：（1）很容易将组合问题转化为SAT。(2)我们可以利用现有的快速SAT算法。在这项研究中，我们首先形式化现实世界的问题，并建立从现实世界的问题到SAT的翻译方法，使自动翻译成为可能。接下来，为了检验我们的方法的效率，我们进行了实验。我们采用了时间安排问题和学生分配问题，这是在大学中流行的问题。我们的实验结果表明，对于这两个问题，我们的方法表现得更好，比现有的直接算法。最后，我们试图通过并行化的SAT的局部搜索算法的加速。我们使用矢量计算机VPP800和PVM。局部搜索算法的性质适合并行化，因为我们可以独立地运行多个搜索路径。此外，我们需要很少的沟通。实验表明，该算法能够获得理想的加速比。我们尝试了几个基准实例，并能够解决一些没有被任何算法解决的实例。

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.