Improving the impact and effectiveness of solvers for complete problems

计算完备性的概念可以通过开发完整问题的求解器来作为实际计算的强大范例。然后，这些求解器可以通过相对简单的编码设备来解决许多其他问题（那些属于同一复杂性类的问题）。这种方法可以被看作是线性规划成功的基础：各种各样的问题可以被编码为线性规划（LP），然后用LP求解器求解。它也是约束满足问题（CSP）的基础，CSP是一个NP完全问题：广泛的重要实际问题可以编码为CSP。近年来，随着构建有效的可满足性（SAT）求解器的新技术的出现，这种范式获得了进一步的发展势头：SAT编码已被证明是解决许多以前需要专门算法的问题的最有效方法。

The notion of computational completeness can be exploited as a powerful paradigm for practical computing by developing solvers for complete problems. These solvers can then be used to solve a number of other problems (those that lie in the same complexity class) by the relatively simple device of encoding. This approach can be seen as underlying the success of linear programming: a wide variety of problems can be encoded as linear programs (LP) and then solved with an LP solver. It is also the basis of Constraint Satisfaction Problems (CSPs) which are an NP-complete problem: a wide range of important practical problems can be encoded as a CSP. In recent years this paradigm has gained further momentum with the advent of new techniques for constructing effective solvers for satisfiability (SAT): encoding to SAT has shown itself to be the most effective way of solving a number of problems that previously required specialized algorithms.