Improving the impact and effectiveness of solvers for complete problems

计算完备性的概念可以通过开发完整问题的求解器作为实用计算的强大范例加以利用。然后，这些求解器可以通过相对简单的编码装置用于解决许多其他问题（那些属于同一复杂性类的问题）。这种方法可以看作是线性规划成功的基础：各种各样的问题可以被编码为线性规划（LP），然后用LP求解器求解。它也是约束满足问题的基础，约束满足问题是一个np完全问题：许多重要的实际问题都可以被编码为约束满足问题。近年来，随着构建可满足性（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.