Improving the impact and effectiveness of solvers for complete problems

点击翻译按钮获取中文摘要

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.