RI: Small: Automated Optimization of Programs and Processing Tools in Answer Set Programming

回答集编程（ASP）是一种知识表示和声明性约束编程的形式，用于表示和解决约束满足问题。 ASP的根源在于需要为复杂的知识密集型应用程序支持快速设计健壮可靠的软件解决方案。它提供了一个高级编程范例，用于将应用领域建模为逻辑语言中的理论，并将所有计算问题留给自动推理。ASP已被用于各种科学和工业应用，包括产品配置，决策支持系统和修复大规模生物网络。这个项目的目的是提高ASP问题的特定编码，以及底层自动推理器或求解器的性能。该项目侧重于三个相关的研究重点，每一个都利用了ASP的高级问题描述。 1)程序重写的研究将为给定的问题生成替代编码; 2）求解器组合的开发将提高整体推理性能，并通过ASP域编码的替代求解器的可用性提供鲁棒性; 3）将研究参数调整以提高单个求解器的性能。 该项目将建立一个评价平台，以系统地实施和验证每一项研究活动。这个评估平台将包括实验编码和一系列来自约束满足和逻辑编程技术的基准问题以及相关的求解器竞赛。

Answer Set Programming (ASP) is a form of knowledge representation and declarative constraint programming used to represent and solve constraint satisfaction problems. ASP has its roots in the need to support fast design of robust and reliable software solutions for complex knowledge-intensive applications. It provides a high-level programming paradigm for modeling an application domain as a theory in a language of logic, and leaves all computational concerns to automated reasoning. ASP has been used in a variety of scientific and industrial applications, including product configuration, decision support systems, and repairing large-scale biological networks. This project aims to improve both the specific encoding of the ASP problems, and the performance of the underlying automated reasoner or solver. The project focuses on three related research thrusts, each of which leverages the high-level problem description of ASP. 1) Research in program rewriting will generate alternative encodings for a given problem; 2) the development of solver portfolios will improve overall reasoning performance and provide robustness through availability of alternate solvers for the ASP domain encodings; and 3) parameter tuning will be investigated to improve the performance of individual solvers. The project will establish an evaluation platform to systematically implement and validate each of these research activities. This evaluation platform will be comprised of both experiment encodings and a collection of benchmark problems from techniques in constraint satisfaction and logic programming as well as related solver competitions.