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.