SHF: Small: From Declarative Specifications of Search Problems to Efficient Solutions

搜索是许多智能软件系统使用的基本技术之一。在程序员用来描述问题的语言和适合求解者进行搜索的编码之间存在着巨大的鸿沟。本研究旨在通过设计和实现将组合问题的声明性规范转换为有效编码的算法来缩小差距。智力上的优点是新颖的框架和算法，用于将规划规范转换为复杂和有效的表逻辑程序，以及将高级约束编译为SAT（可满足性）编码的前沿算法。该项目更广泛的意义和重要性在于，它有可能产生持久的、重大的经济、教育和社会影响，因为组合问题无处不在，由此产生的理论和原型将形成技术，使未来的系统能够获得各种组合问题的高质量解决方案。本研究将重点关注两种类型的组合问题：人工智能规划和使用SAT解决的约束满足问题。表逻辑编程已被证明是一种强大而灵活的规划问题建模和求解语言。然而，在表逻辑编程中开发有效的规划模型是一门艺术，而不是一门科学。本研究设计的用于将规划规范转换为有效的表逻辑程序的算法将具有以下功能：(1)将状态的因子表示转换为利用对称性的结构表示；(2)提取领域相关的控制知识，如确定性行为和部分顺序；(3)学习表征特异性启发式。全局约束是约束规划的重要组成部分。它们不仅可以方便地对许多问题进行建模，而且还可以使用强大的传播算法。针对一些全局约束，已经提出了SAT编码算法。然而，目前还没有成熟的算法将全局约束编码到SAT中；许多其他的全局约束，如图约束，尽管在实际应用中很有用，但却没有得到太多的关注。这项研究将产生一套全面的全局约束算法，并将基于这些算法开发一个前沿的约束求解系统。

Search is one of the fundamental techniques used by many intelligent software systems. There is a big chasm between the languages that programmers use to describe problems and the encodings that are suitable for solvers to conduct search. This research aims to narrow the gap by designing and implementing algorithms for translating declarative specifications of combinatorial problems into efficient encodings. The intellectual merits are novel frameworks and algorithms for translating planning specifications into sophisticated and efficient tabled logic programs, and cutting-edge algorithms for compiling high-level constraints into SAT (satisfiability) encodings. The project's broader significance and importance are its potential to produce long-lasting, significant economic, educational, and social impact because of the ubiquity of combinatorial problems, and the resulting theory and prototypes that will form the technology which enables future systems to obtain high-quality solutions to a variety of combinatorial problems. This research will focus on two types of combinatorial problems: AI planning and constraint satisfaction problems solved using SAT. Tabled logic programming has been shown to be a powerful and flexible modeling and solving language for planning problems. Nevertheless, it is an art, not a science, to develop efficient planning models in tabled logic programming. The algorithms designed by this research for translating planning specifications into efficient tabled logic programs will have the following capabilities: (1) convert factored representations of states into structural representations that exploit symmetries; (2) extract domain-dependent control knowledge, such as deterministic actions and partial orders; and (3) learn representation-specific heuristics. Global constraints are an important part of constraint programming. They not only allow easy modeling of many problems, but also enable use of powerful propagation algorithms. SAT encoding algorithms have been proposed for some of the global constraints. Nevertheless, there are no well-established algorithms for encoding global constraints into SAT; many other global constraints, such as graph constraints, have not received much attention despite their usefulness in practical applications. This research will produce algorithms for a comprehensive set of global constraints, and will develop a cutting-edge constraint-solving system based on these algorithms.