Compiling Knowledge for Tractable and Embedded Inference

知识编译是近年来出现的一个新的研究方向，用于解决一般命题推理的计算难题。 在这种方法中，推理过程分为两个阶段：离线编译阶段和在线问答阶段。 在离线阶段，命题理论被编译成某种目标语言，这通常是一种易于处理的语言。在联机阶段，编译目标用于有效地回答（潜在的）指数数量的查询。 知识编译背后的主要动机是将尽可能多的计算开销推到离线阶段，以便将该开销分摊到所有在线查询上。 编译的另一个动机是产生非常简单的在线推理系统，这些系统可以被低成本地嵌入到原始的计算平台中，例如消费电子产品中的计算平台。（与Horn理论相反），支持比Horn理论和素数蕴涵更多的多项式时间运算，比OBDD更节省空间，并且就其结构和算法而言非常简单。 因此，DNNF代表了一个新的，有趣的点上的四维结构的普遍性，易处理性，效率和简单性。 多项式时间DNNF运算类足以完全实现相对复杂的AI应用程序，例如基于模型的诊断器和通用规划器。 此外，鉴于OBDD社区目前在编译相当复杂的命题理论方面取得的成功，它的空间效率为基于DNNF的编译的有效性建立了一个非常重要的底线。第一个，也是最核心的目标，是沿着沿着三个维度推进DNNF编译信封： 开发生成比目前可能的小得多的DNNF编译的算法; 开发一个DNNF编译器，它可以根据底层理论的增量变化来增量地改变DNNF编译; 并开发近似DNNFs的理论，其可用于仅回答预定类别的查询。 第二个目标是追求DNNFs的适用性，以编制通用的规划师，这是一个目标，这是可能的最新进展的满意度为基础的规划。 第三个目标是使用现场可编程门阵列（FPGA）开发一些DNNF操作的硬件实现，以便允许将某些诊断和规划应用程序编译为硬件。 本计划的第四个目标是对一些必要的理论基础进行调查，以充分理解DNNF和其他易于处理的形式之间的关系，如霍恩理论和OBDDs。该项目将对智能系统中的命题推理的理论和实践产生重大影响。 在理论方面，它将揭示命题推理的可编译性和各种目标编译语言之间的关系，如OBDDs，Horn理论和素数蕴涵。 在实践方面，它将产生比目前更容易处理的在线推理系统，并将使某些人工智能应用程序（特别是诊断和规划）迁移到具有原始计算资源的平台上。 这可能为嵌入式智能提供了坚实的基础，就像在命题推理的强大框架中练习一样。

Knowledge compilation has been emerging recently as a new direction of research for dealing with the computational intractability of general propositional reasoning. In this approach, the reasoning process is split into two phases: an off-line compilation phase and an on-line query-answering phase. In the off-line phase the propositional theory is compiled into some target language, which is typically a tractable one. In the on-line phase, the compiled target is used to efficiently answer a (potentially) exponential number of queries. The main motivation behind knowledge compilation is to push as much of the computational overhead as possible into the off-line phase, in order to amortize that overhead over all on-line queries. Another motivation behind compilation is to produce very simplistic on-line reasoning systems, which can be embedded cost-effectively into primitive computational platforms, such as those found in consumer electronics.The focus of this research is on a new compilation target language, known as Decomposable Negation Normal Form (DNNF) which is universal (contrary to Horn theories), supports more polynomial-time operations than Horn theories and prime implicates, is more space-efficient than OBDDs, and is very simplistic as far as its structure and algorithms are concerned. Therefore, DNNF represents a new, interesting point on the four-dimensional structure of universality, tractability, efficiency and simplicity. The class of polynomial-time DNNF operations is sufficient to fully implement relatively complex AI applications, such as model-based diagnosers and universal planners. Moreover, its space-efficiency establishes a very significant bottom-line for the effectiveness of DNNF-based compilations, given the current success of the OBDD community in compiling quite complex propositional theories.There are four major objectives of this proposal. The first, and most central objective, is to push the DNNF compilation envelope along three dimensions: to develop algorithms that generate much smaller DNNF compilations than is currently possible; to develop a DNNF compiler which can incrementally change a DNNF compilation in light of incremental changes to the underlying theory; and to develop the theory of approximate DNNFs, which can be used to answer only a predetermined class of queries. The second objective is to pursue the applicability of DNNFs to the compilation of universal planners, an objective which is made possible by recent advances on satisfiability-based planning. The third objective is to develop a hardware implementation of some DNNF operations using Field Programmable Gate Arrays (FPGAs) in order to permit the compilation of certain diagnosis and planning applications into hardware. The fourth objective of this proposal is to conduct an investigation on some of the theoretical underpinnings necessary to fully understand the relationship between DNNF and other tractable forms, such as Horn theories and OBDDs.This project will make a strong impact on the theory and practice of propositional reasoning in intelligent systems. On the theoretical side, it will shed new light on the compilability of propositional reasoning and on the relationship between various target compilation languages, such as OBDDs, Horn theories and prime implicates. On the practical side, it will yield on-line reasoning systems which are more tractable than is currently possible, and will enable the migration of certain AI applications (diagnosis and planning in particular) onto platforms with primitive computational resources. This may provide a solid foundation for embedded intelligence, as exercised in the powerful framework of propositional reasoning.