算法工程的思想、方法与工具——以SAT算法为研究实例

The Theory, Methodology and Tools of Algorithm Engineering: A Case Study with SAT Algorithms

1.什么是"算法工程"? 20世纪90年代中期,"算法工程"这个词开始频频出现.A.V.Aho等计算机科学家曾在1996年ACM计算理论研讨会(STOC'96)上呼吁研究者们要重视算法工程的研究和实践[1].

The recently emerging idea of Algorithm Engineering in the community of Computer Science is about how to engineer computer algorithms by integrating the design, analysis, implementation, experimental testing, refinement, etc. of them, aiming at improving their runtime performance. In this paper, we try to develop the main idea of the theory and methodology of algorithm engineering, and give an introduction to some useful tools. In order to concretize our discussion and illustrate the effectiveness of algorithm engineering, we will base our study on the engineering of SAT algorithms. According to the rules and methodologies of algorithm engineering we have learned, we implement a simple but efficient SAT solver, QuickSAT, as a testbed. Although we haven't utilized most of the advanced techniques used in modern SAT solvers, the result of experimental comparison shows that QuickSAT is close in performance to zChaff, one of the leading SAT solvers in the world today.