Exploiting Structure in Satisfiability-Based Problem Solving

随机组合问题，包括许多优化问题，出现在几乎所有的科学，工程和商业领域，以及应用计算机科学。 解决这些问题的软件的一种特殊方法，有时称为基于可满足性或基于约束的问题解决，为面临这些问题的工作人员提供了建模和解决能力。 用户谁不是专家在组合问题解决只需要描述他们的问题，在一个高层次的，声明性的，规范语言，以获得解决方案。 基于这种方法的技术是非常新的，但正在被证明对越来越多的问题非常有效。 这项研究旨在解决当前技术的两个重要局限性。 一个是，目前还不知道如何调整该技术核心的求解算法，以利用未来十年可以预期的非常高性能的硬件，涉及非常大量的计算核心和可能的绝热量子退火处理器。 第二个问题是，有一个范围广泛的问题，其中最有效的算法被称为动态规划算法，但模型和解决技术没有利用这一点。 虽然性质不同，但这两个问题都可以部分地通过利用问题实例的特定结构属性的一般方法来解决。 然而，在实践中利用这些特性需要新的理论和算法，这就是本项目的主题。

Challenging combinatorial problems, including many optimization problems, arise in almost all areas of science, engineering and business, and applied computer science.  A particular approach to software for solving these problems, sometimes called satisfiability-based or constraint-based problem solving, provides workers facing such problems with a model-and-solve capability.  Users who are not experts in combinatorial problem solving need only describe their problem in a high-level, declarative, specification language to obtain solutions.  Technology based on this approach is very new, but is being shown highly effective for a growing range of problems.  This research aims to address two important limitations of the current technology.  One is that it is unknown how to adapt the solving algorithms at the core of this technology to exploit very high performance hardware which can be expected in the next decade, involving either very large numbers of compute cores and possibly adiabatic quantum annealing processors.  The second is that there is a wide range of problems for which the most effective algorithms are known as dynamic programming algorithms, but mode-and-solve technologies do not exploit this.  While of a different nature, both of these problems may be addressed in part by general methods which exploit particular structural properties of problem instances.  Taking advantage of these properties in practice, though, required new theory and algorithms, which are the subject of this project.