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.