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. The proposed research aims to further expand the impact and effectiveness of this paradigm in two different ways. First, research on more effective algorithms for various complete problems will be continued. In previous work new algorithms for solving #SAT (complete for #P), Soft-CSPs (complete for APX), and QBF (complete for PSPACE) have been created and used to develop more effective solvers for these problems. In new research previous ideas will be further developed and new ideas, especially for MAXSAT and QBF, will be explored. By examining a range of different complete problems the applicability of the encoding approach can be expanded. Second, the research will look at developing a higher-level declarative language for representing problems. The aim is to develop a modeling language and system with which users can more easily and naturally express and solve their problems. The proposed research is expected to further the effectiveness and usefulness of solvers for a range of complete problems, and thus is expected to have a significant impact on a range of applications both in industry and in science.