Solving combinatorial problems by grounding from specifications

组合搜索和优化问题是一个普遍存在的问题。一些例子包括查找考试时间表，调度机器，构建系统发育树，配置复杂系统，以及查找计算机系统中的错误。 这些问题中的大多数属于一类问题（称为NP完全问题），对于这类问题，不存在保证有效的已知算法，而且，在实践中出现的情况往往不能在合理的时间内通过当前的方法解决。因此，它们提出了重大的科学和实际挑战。 拟议的研究旨在开发新的方法来处理这些问题，特别是解决两个问题，目前的最先进的组合问题解决方法。 首先，虽然目前的算法和计算机能够轻松地为许多领域的工人面临的许多问题提供解决方案，但这样做的技术对这些工人中的许多人来说是不可访问的，甚至是未知的。 一个主要的目标是开发方法，更容易获得，特别是通过提供建模语言和软件工具，允许复杂的底层计算资源被使用的工人谁不是专家在组合问题解决。 第二，尽管主流技术高度发达，并以数十年的高质量科学为基础，但仍有一些领域现有的最佳组合求解方法不能有效或稳健地工作。 另一个目标是进一步开发一种新的算法方法来解决这些问题，并利用具有多个核心的计算机处理器-这将很快出现在标准台式计算机中-来解决这些问题。在我们的方法中，建模语言和计算求解方法都基于数学逻辑中的底层形式化，这在理论和实际工作中都提供了许多好处。

Challenging combinatorial search and optimization problems are ubiquitous and diverse. A few examples include finding exam timetables, scheduling machines, constructing phylogenetic trees, configuring complex systems, and finding bugs in computer systems. Most of these problems belong to a class of problems (known as the NP-complete problems) for which no known algorithms exist which are guaranteed to be efficient, and moreover, instances that arise in practice often cannot be solved by current methods in reasonable time. They thus present major scientific and practical challenges. The proposed research aims to develop new methods for handling such problems, in particular addressing two issues with the current state-of-the-art in combinatorial problem solving methods. First, while current algorithms and computers are able to easily produce solutions for many problems that workers in many areas face, the technology to do so is not accessible to - or even known to - many of these workers. A primary goal is to develop methods that are much more accessible, in particular by providing modelling languages and software tools which allow complex underlying computational resources to be used by workers who are not specialists in combinatorial problem solving. Second, there remain a number of areas where the best existing combinatorial solving methods do not work effectively or robustly, in spite of the fact that the mainstream technologies are highly developed and based on decades of high quality science. Another goal is to further develop a newer algorithmic approach for solving such problems, and for exploiting computer processors with many cores - which will soon be in standard desktop computers - in the service of solving these problems. In our approach, both modelling languages and computational solving methods are based on an underlying formalization in mathematical logic, which provides a number of benefits in both theoretical and practical work.