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.