Collaborative Research: SAIL: An Integration of SAT Solver and Inductive Prover

合作研究：SAIL：SAT 求解器和归纳证明器的集成

• 批准号: 0541070
• 负责人: Hantao Zhang
• 金额: $ 9.95万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-09-15 至 2011-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0541070&HistoricalAwards=false
• 关键词: Collaborative; Research; SAIL; Integration; SAT

Below is the abstract for these three collaborative proposals.This project works toward theoretical advances in reasoning techniques to improve software design. Recent advances in SAT solvers, design of decision procedures, framework for combining decision procedures, and automatic methods for inductive reasoning have opened possibilities for creating reasoning systems that are more powerful than the individual techniques. Most of the work of the project is to integrate them into a common workbench, called SAIL (A SAT and Induction Laboratory), which can serve as a powerful tool for design of software and hardware. SAIL will incorporate decision procedures for several commonly used theories including theories of equality over uninterpreted symbols, free constructors, and Presburger arithmetic. In addition, procedures for integrating induction into decision procedures without losing automation will be supported. A new approach for reuse of SAT techniques by creating a library called SatBox will be developed. SAIL will include a new flexible, modular approach based on SatBox to integrate the decision procedures into a SAT solver based on the Davis, Putnam, Logemann and Loveland (DPLL) framework. Theoretical and experimental advances will be made in the areas of combining decision procedures and for guiding interactions between simplification, decision procedures, SAT solvers, and induction theorem proving. The design and implementation of SAIL will be guided by applying it on varied software design applications. The broader impacts of the work are long-term, leading to improvements in quality of software and software development processes. The theory and tools have broad applications.

以下是这三个合作提案的摘要。该项目致力于推理技术的理论进步，以改进软件设计。 SAT 求解器、决策过程的设计、组合决策过程的框架以及归纳推理的自动方法的最新进展为创建比单独技术更强大的推理系统提供了可能性。 该项目的大部分工作是将它们集成到一个通用工作台中，称为SAIL（A SAT and Induction Laboratory），它可以作为软件和硬件设计的强大工具。 SAIL 将纳入几种常用理论的决策程序，包括未解释符号的相等理论、自由构造函数和 Presburger 算术。此外，还将支持将归纳法整合到决策程序中而不失去自动化的程序。 将开发一种通过创建名为 SatBox 的库来重用 SAT 技术的新方法。 SAIL 将包括一种基于 SatBox 的新的灵活模块化方法，将决策程序集成到基于 Davis、Putnam、Logemann 和 Loveland (DPLL) 框架的 SAT 求解器中。将在组合决策程序以及指导简化、决策程序、SAT 求解器和归纳定理证明之间的交互方面取得理论和实验进展。 SAIL 的设计和实现将通过将其应用于各种软件设计应用程序来指导。这项工作的更广泛的影响是长期的，从而提高软件和软件开发过程的质量。该理论和工具具有广泛的应用。