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

这项研究的目的是开发解决现实世界中棘手问题的一般方法。我们的策略不是直接解决每个问题，而是将其转化为CNF可满足性(SAT)，求解SAT，并将SAT的解转换回原始问题的解。我们可以预料到几个优点：(1)将组合问题转化为SAT很容易。(2)可以利用已有的快速SAT算法。在本研究中，我们首先将现实问题形式化，并建立了从现实问题到SAT的转换方法，从而使自动翻译成为可能。其次，为了验证该方法的效率，我们进行了实验。我们采用了时间调度问题和学生分配问题，这两个问题在大学里很常见。实验结果表明，对于这两个问题，我们的方法都优于已有的直接算法。最后，我们尝试通过并行化来加速SAT的局部搜索算法。为此，我们使用了矢量计算机VPP 800和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.