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

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, refine-ment, 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 givean 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, Quick SAT, 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 Quick SAT is close in performance to zChaff, one of the leading SAT solvers in the world to-day.

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

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.