Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories
Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories
复制标题
DOI：
10.1145/1838552.1838559
复制
发表时间：
2010-10-01
影响因子：
0.5
通讯作者：
Sebastiani, Roberto
中科院分区：
文献类型：
--
作者：
Cimatti, Alessandro;Griggio, Alberto;Sebastiani, Roberto
计算Craig interpolants的问题最近引起了很多兴趣。在本文中，我们解决了有效产生插值的问题的问题，用于一阶逻辑的一些重要片段，这些逻辑可用于有效的决策程序，称为“满意度”理论（SMT）求解器。我们做出以下贡献。首先，我们为几种基本感兴趣的基本理论提供了插值程序：关于理性的线性算术理论，对理由和整数的差异逻辑，以及对理由和整数的UTVPI。其次，我们定义了一种新的方法来插入理论的插值组合，该方法适用于延迟理论组合方法。通过以下事实确保了效率，即提出的插值算法扩展了最先进的算法，以实现满意度理论。我们的实验评估表明，与其他竞争对手求解器相比，MathSAT SMT求解器可以产生带有较小开销的室内介质，并且比其他竞争对手求解器更有效。
The problem of computing Craig interpolants has recently received a lot of interest. In this article, we address the problem of efficient generation of interpolants for some important fragments of first-order logic, which are amenable for effective decision procedures, called satisfiability modulo theory (SMT) solvers.We make the following contributions. First, we provide interpolation procedures for several basic theories of interest: the theories of linear arithmetic over the rationals, difference logic over rationals and integers, and UTVPI over rationals and integers. Second, we define a novel approach to interpolate combinations of theories that applies to the delayed theory combination approach.Efficiency is ensured by the fact that the proposed interpolation algorithms extend state-of-the-art algorithms for satisfiability modulo theories. Our experimental evaluation shows that the MathSAT SMT solver can produce interpolants with minor overhead in search, and much more efficiently than other competitor solvers.