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.