Improving the impact and effectiveness of solvers for complete problems

通过开发完全问题的解算器，计算完备性的概念可以被用作实际计算的强大范例。然后，这些解算器可以通过相对简单的编码设备来解决许多其他问题(属于同一复杂类别的问题)。这种方法可以被视为线性规划成功的基础：各种各样的问题可以被编码为线性规划(LP)，然后用线性规划求解器求解。它也是约束满足问题(CSP)的基础，约束满足问题是一个NP-完全问题：许多重要的实际问题都可以编码为CSP。近年来，随着构造有效的可满足性求解器(SAT)的新技术的出现，这一范例得到了进一步的发展：编码到SAT已被证明是解决许多以前需要专门算法的问题的最有效的方法。 这项拟议的研究旨在通过两种不同的方式进一步扩大这一范式的影响和有效性。首先，将继续研究更有效的算法来解决各种完全问题。在以前的工作中，已经创建了用于解决#SAT(对#P完成)、软CSP(对APX完成)和QBF(对PSPACE完成)的新算法，并用于开发针对这些问题的更有效的解算器。在新的研究中，将进一步发展以前的想法，并探索新的想法，特别是在MAXSAT和QBF方面。通过检查一系列不同的完全问题，可以扩展编码方法的适用性。其次，这项研究将着眼于开发一种更高级别的陈述性语言来表示问题。其目的是开发一种建模语言和系统，使用户可以更容易、更自然地表达和解决他们的问题。预计拟议的研究将进一步提高解决一系列完整问题的有效性和有用性，从而有望对工业和科学中的一系列应用产生重大影响。

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.