Model expansion as a framework for representing and solving search and optimization problems

计算困难的搜索和优化问题在科学、工程和商业中无处不在。例子包括药物设计、蛋白质折叠、系统发育重建、硬件和软件设计、测试生成和验证、计划、时间表、调度等。在极少数情况下，实际的特定于应用程序的软件是存在的，但大多数情况下，成功方法的开发需要雇佣专家，并且通常需要大量的时间和费用来应用一种或多种计算方法。这个项目的目标是为解决搜索和优化问题的各种方法建立正式的基础和统一的原则。这项研究将有助于发展一种对用户的专门知识要求相当少的办法，从而使解决这类问题的技术为更广泛的用户所利用。在这种方法中，用户用声明性建模语言给出他们的搜索（或优化）问题的精确说明，例如经典一阶逻辑的扩展或类似于众所周知的数据库查询语言SQL的语言。然后，求解器将此规范与问题的实例（即存储在数据库中的数据）结合起来，并生成问题的解决方案（如果有的话）。我们承担了理论发展和通过系统开发证明实际可行性的研究计划。

Computationally hard search and optimization problems are ubiquitous in science, engineering and business. Examples include drug design, protein folding, phylogeny reconstruction, hardware and software design, test generation and verification, planning, timetabling, scheduling and so on. In rare cases, practical application-specific software exists, but most often development of successful methods requires hiring specialists, and often significant time and expense, to apply one or more computational approaches. The goal of this project is to develop formal foundations and unifying principles of various methods of solving search and optimization problems.The research will help developing an approach which would require considerably less specialized expertise on the part of the user, thus making technology for solving such problems accessible to a wider variety of users. In this approach, the user gives a precise specification of their search (or optimization) problem in a declarative modelling language, for example an extension of classical first-order logic or a language similar to the well-known database query language SQL. A solver then takes this specification, together with an instance of the problem (i.e., data stored in a database), and produces a solution to the problem (if there is one). We undertake a research program of both theoretical development and demonstrating practical feasibility through system development.