Exploiting Structure in Satisfiability-Based Problem Solving

在基于可满足性的问题解决中利用结构

• 批准号: RGPIN-2015-05855
• 负责人: Mitchell, David
• 金额: $ 1.75万
• 依托单位: Simon Fraser University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=679720
• 关键词: Exploiting; Structure; Satisfiability; Based; Problem

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.

在科学，工程和商业的几乎所有领域以及应用计算机科学的几乎所有领域都出现了具有挑战性的组合问题，包括许多优化问题。解决这些问题的特定软件方法，有时称为基于满意度或基于约束的问题解决，可以通过模型和解决能力面对此类问题的工人。不是组合问题的专家的用户只需要用高级，声明性的规范语言来描述其问题，以获取解决方案。基于这种方法的技术非常新，但对越来越多的问题表现出非常有效的表现。这项研究旨在解决当前技术的两个重要局限性。一个是，未知如何适应该技术核心的求解算法来探索非常高的性能硬件，这在未来十年中可以预期，涉及大量的计算核心以及可能是绝热的量子退火处理器。第二个是最有效的算法被称为动态编程算法的广泛问题，但是模式和解决技术并不能利用这一点。尽管性质不同，但这两个问题都可以部分通过利用问题实例的特定结构特性的一般方法来解决。但是，利用这些属性在实践中需要新的理论和算法，这是该项目的主题。